Skip to content
  • Amin Timany's avatar
    Squashed commit of the following: · f1ae6242
    Amin Timany authored
    commit 392b7b43
    Author: Amin Timany <amintimany@gmail.com>
    Date:   Tue May 3 21:25:10 2016 +0200
    
        Finish using new iris with "proof mode"
    
        In Fμ and Fμ_ref we do support reduction under Fold.
        In fact `Unfold (Fold v)` is reduced to `v` if and only if v is a variable.
    
    commit 9825e341
    Author: Amin Timany <amintimany@gmail.com>
    Date:   Mon May 2 20:35:57 2016 +0200
    
        Prove fundamental lemma of stlc is proven
    
        Change the Fμ to make the operational semantics reduce under Fold.
        Fundamental lemma for Fμ is partially proven (up to App).
    f1ae6242