Extensibella Example: soundX:pair

Language Specification

File: def.sos

[Reduce File] [Raw File] 
Module soundX:pair

Builds on soundX:host

tm ::= ...
     | pair(tm, tm)
     | fst(tm)
     | snd(tm)


ty ::= ...
     | pairTy(ty)


typeOf Ctx T1 Ty
----------------------------------------------------------- [Proj-Pair]
Ctx |{tm}- pair(T1, T2) ~~>
     app(
       app(
         abs("A", Ty, abs("B", Ty,
             abs("S", arrowTy(Ty, arrowTy(Ty, Ty)),
                 app(app(var("S"), var("A")), var("B"))))),
         T1),
       T2)


typeOf Ctx T pairTy(Ty)
------------------------------------------------- [Proj-Fst]
Ctx |{tm}- fst(T) ~~>
     app(T, abs("A", Ty, abs("B", Ty, var("A"))))


typeOf Ctx T pairTy(Ty)
------------------------------------------------- [Proj-Snd]
Ctx |{tm}- snd(T) ~~>
     app(T, abs("A", Ty, abs("B", Ty, var("B"))))


------------------------------------------------ [Proj-PairTy]
|{ty}- pairTy(Ty) ~~>
       arrowTy(arrowTy(Ty, arrowTy(Ty, Ty)), Ty)



typeOf Ctx T1 Ty
typeOf Ctx T2 Ty
---------------------------------- [T-Pair]
typeOf Ctx pair(T1, T2) pairTy(Ty)


typeOf Ctx T pairTy(Ty)
----------------------- [T-Fst]
typeOf Ctx fst(T) Ty


typeOf Ctx T pairTy(Ty)
----------------------- [T-Snd]
typeOf Ctx snd(T) Ty

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:pair.

Prove_Constraint soundX:host:proj_ty_is. [Show Proof]



Prove soundX:host:type_is. [Show Proof]



Prove_Constraint soundX:host:proj_is. [Show Proof]



Prove soundX:host:type_unique. [Show Proof]



Prove soundX:host:ty_lookup. [Show Proof]



Prove_Constraint soundX:host:proj_ty_unique. [Show Proof]



Prove_Constraint soundX:host:proj_tm_unique. [Show Proof]






Prove soundX:host:desugar_ty_exists. [Show Proof]



Prove soundX:host:desugar_ty_rel. [Show Proof]
Back to example home