% % Elaboration Type Soundness % elab-type-soundness : % If elab E A M % Gamma |- e : A `--> M % then -> typeoftm M A % ||Gamma|| |- M : ||A|| -> type. %mode elab-type-soundness +Elab -D. %block elab-type-soundnessblock : some {A : ty} block {e : exp} {m : tm} {Elab : elab e A m} {Typetm : typeoftm m A} {_ : elab-type-soundness Elab Typetm}. - : elab-type-soundness (elab/topintro IsVal) (typeoftm/unitintro). - : elab-type-soundness (elab/arrelim Elab1 (Elab2 : elab E Aarg Marg)) (typeoftm/arrelim D1 D2) <- elab-type-soundness Elab1 D1 <- elab-type-soundness Elab2 D2. - : {A : ty} {B : ty} {DBody : {m : tm} typeoftm m A -> typeoftm (Mbody m) B} {ElabBody : {earg : exp} {m : tm} elab earg A m -> elab (Ebody earg) B (Mbody m)} elab-type-soundness (elab/arrintro ElabBody) (typeoftm/arrintro DBody) <- {earg : exp} {m : tm} {ElabArg : elab earg A m} {DArg : typeoftm m A} {_ : elab-type-soundness ElabArg DArg} elab-type-soundness (ElabBody earg m ElabArg) (DBody m DArg) . - : {A : ty} {DBody : {m : tm} typeoftm m A -> typeoftm (Mbody m) A} {ElabBody : {earg : exp} {m : tm} elab earg A m -> elab (Ebody earg) A (Mbody m)} elab-type-soundness (elab/fix ElabBody) (typeoftm/fix DBody) <- {earg : exp} {m : tm} {ElabArg : elab earg A m} {DArg : typeoftm m A} {_ : elab-type-soundness ElabArg DArg} elab-type-soundness (ElabBody earg m ElabArg) (DBody m DArg) . - : elab-type-soundness (elab/merge1 Elab1) D <- elab-type-soundness Elab1 D. - : elab-type-soundness (elab/merge2 Elab2) D <- elab-type-soundness Elab2 D. - : elab-type-soundness (elab/sectintro Elab1 Elab2) (typeoftm/prodintro D1 D2) <- elab-type-soundness Elab1 D1 <- elab-type-soundness Elab2 D2. - : elab-type-soundness (elab/sectelim1 Elab1) (typeoftm/prodelim1 D) <- elab-type-soundness Elab1 D. - : elab-type-soundness (elab/sectelim2 Elab2) (typeoftm/prodelim2 D) <- elab-type-soundness Elab2 D. - : elab-type-soundness (elab/unintro1 Elab1) (typeoftm/sumintro1 D) <- elab-type-soundness Elab1 D. - : elab-type-soundness (elab/unintro2 Elab2) (typeoftm/sumintro2 D) <- elab-type-soundness Elab2 D. - : elab-type-soundness (elab/unelim Fill Elab' Elab1 Elab2) (typeoftm/sumelim D' D1 D2) <- elab-type-soundness Elab' D' <- ({x1:exp} {m1:tm} {Elabx1:elab x1 A1 m1} {Dm1:typeoftm m1 A1} elab-type-soundness Elabx1 Dm1 -> elab-type-soundness (Elab1 x1 m1 Elabx1) (D1 m1 Dm1) ) <- ({x2:exp} {m2:tm} {Elabx2:elab x2 A2 m2} {Dm2:typeoftm m2 A2} elab-type-soundness Elabx2 Dm2 -> elab-type-soundness (Elab2 x2 m2 Elabx2) (D2 m2 Dm2)) . - : elab-type-soundness (elab/direct Fill Elab' Elab1) (typeoftm/arrelim (typeoftm/arrintro D1) D') <- elab-type-soundness Elab' D' <- ( {x1:exp} {m1:tm} {Elabx1:elab x1 A m1} {Dm1:typeoftm m1 A} elab-type-soundness Elabx1 Dm1 -> elab-type-soundness (Elab1 x1 m1 Elabx1) (D1 m1 Dm1) ) . %worlds (elab-type-soundnessblock) (elab-type-soundness _ _). %total Elab (elab-type-soundness Elab _).