Ignore:
Timestamp:
Jan 5, 2013, 1:41:13 PM (8 years ago)
Author:
piccolo
Message:

ERTLtoERTLptr in place

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/linearise.ma

    r2562 r2570  
    591591qed.
    592592
     593(* spostato in ExtraMonads.ma
    593594lemma option_bind_inverse : ∀A,B.∀m : option A.∀f : A → option B.∀r.
    594595  ! x ← m ; f x = return r →
     
    597598%{x} %{EQ} %
    598599qed.
     600*)
    599601
    600602lemma nth_opt_reverse_hit :
Note: See TracChangeset for help on using the changeset viewer.