Extensibella Example: walkthrough:big_step

Language Specification

File: module.sos

[Reduce File] [Raw File] 
Module walkthrough:big_step

Builds on walkthrough:host


Judgment big_step : tm* tm

value T
------------ [Big-End]
big_step T T


eval T T1
big_step T1 T2
-------------- [Big-Step]
big_step T T2


[] |{tm}- T ~~> T_T
big_step T_T T1
------------------- [Big-D]*
big_step T T1

Reasoning

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

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

Module walkthrough:big_step.


Prove walkthrough:host:typeOf_unique.


Prove walkthrough:host:ty_lookup.


Prove walkthrough:host:subst_type_preservation.


Prove walkthrough:host:type_preservation.


Prove_Constraint walkthrough:host:proj_type_same.


Add_Ext_Size walkthrough:host:eval.


Add_Proj_Rel walkthrough:host:eval.


Prove_Ext_Ind walkthrough:host:eval.


Extensible_Theorem
  big_step_type_preservation : forall T Ty T',
    Ty : typeOf [] T Ty ->
    Big : big_step T T' ->
    typeOf [] T' Ty
  on Big. [Show Proof]
Back to example home