% "Summary" results, which just compose various theorems. % summary-static: If . |- e : A in the full (including subsumption) source typing system, % then there exists e' such that . |- e' : A elaborates to M % and . |- M : A in the target type system. summary-static : % If typeof+sub E A % then -> elab E' A M -> typeoftm M A -> type. %mode summary-static +DwithSubsumption -Elab -Dtarget. - : summary-static DwithSubsumption Elab Dtarget <- coerce E DwithSubsumption EwithCoercions DwithCoercions <- elab-complete DwithCoercions Elab <- elab-type-soundness Elab Dtarget. %worlds () (summary-static _ _ _). %total {} (summary-static _ _ _). % summary-dynamic: If . |- e : A elaborates to M % and M evaluates to a value W (in zero or more steps) % then there exists v such that: % e steps to v in zero or more steps % and . |- v : A. summary-dynamic : % If {E : exp} elab E A M -> steptm* M W -> is-valuetm W % then there exists a value V -> {V : exp} is-value V % such that E steps to V, -> step* E V % preserving types. -> typeof V A -> type. %mode summary-dynamic +E +ElabE +Step*MW +IsValtmW -V -IsVal -Step*EV -TypeofV. - : summary-dynamic E ElabE Step*MW IsValtmW V IsVal Step*EV TypeofV <- consistency* ElabE IsValtmW Step*MW Step*EV IsVal ElabV <- typeof-erase TypeofV ElabV. %worlds () (summary-dynamic _ _ _ _ _ _ _ _). %total {} (summary-dynamic _ _ _ _ _ _ _ _).