Extensibella Example: soundX:let

Language Specification

File: def.sos

Module soundX:let

Builds on soundX:host

tm ::= ...
     | let(string, tm, tm)


typeOf Ctx T1 Ty
----------------------------------------------------- [Proj-Let]
Ctx |{tm}- let(X, T1, T2) ~~> app(abs(X, Ty, T2), T1)



typeOf Ctx T1 Ty1
typeOf (X, Ty1)::Ctx T2 Ty2
----------------------------- [T-Let]
typeOf Ctx let(X, T1, T2) Ty2

Reasoning

[Show All Proofs] [Hide All Proofs] [Raw File]

Click on a command or tactic to see a detailed view of its use.

Module soundX:let.

Prove_Constraint soundX:host:proj_ty_is.


Prove soundX:host:type_is. [Show Proof]

%T-Let
 Is: case IsT. apply IH to _ Is1 Ty1. apply IH to _ Is2 Ty2. search.


Prove_Constraint soundX:host:proj_is. [Show Proof]

%Proj-Let
 case IsT. apply type_is to _ _ Proj1. search.


Prove soundX:host:type_unique. [Show Proof]

%T-Let
 TyB: case TyB. case IsT. apply IH to _ _ TyA1 TyB.
 apply type_is to _ _ TyA1. apply IH to _ _ TyA2 TyB1. search.


Prove soundX:host:ty_lookup. [Show Proof]

%T-Let
 apply IH to Ty1 L. apply IH to Ty2 _ with Ctx2 = (X, Ty1)::Ctx2.
   intros Lkp. Lkp: case Lkp.
     %Lkp-Here
      search.
     %Lkp-Later
      apply L to Lkp1. search.
 search.


Prove_Constraint soundX:host:proj_ty_unique.


Prove_Constraint soundX:host:proj_tm_unique. [Show Proof]

%Proj-Let
 case Hyp1. case Hyp2. apply type_unique to _ _ Hyp4 H1. search.




Prove soundX:host:desugar_ty_exists.


Prove soundX:host:desugar_ty_rel. [Show Proof]

%T-Let
 case IsT. DT: case DT. DT: case DT. DT: case DT1. DT: case DT1.
 apply type_unique to _ _ DT Ty1. apply IH to _ _ Ty1 _ _ _.
 apply type_is to _ _ Ty1. apply IH to _ _ Ty2 _ _ _. search.
 %clear impossible cases
 case DT1. case DT1.

Back to example home