Changeset 1647 for src/utilities/option.ma
 Timestamp:
 Jan 17, 2012, 1:13:08 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/utilities/option.ma
r1640 r1647 2 2 include "basics/types.ma". 3 3 4 definition Option ≝ MakeMonad (mk_MonadDefinition4 definition Option ≝ MakeMonadProps 5 5 (* the monad *) 6 6 option … … 9 9 (* bind *) 10 10 (λX,Y,m,f. match m with [ Some x ⇒ f x  None ⇒ None ?]) 11 ??? ).12 // #X[ #Y#Z]*normalize//qed.11 ???. 12 // #X[2:#Y#Z]*normalize//qed. 13 13 14 14 include "hints_declaration.ma". 15 15 unification hint 0 ≔ X; 16 M ≟ m_def Option 16 N ≟ max_def Option, M ≟ m_def N 17 17 (**) ⊢ 18 18 option X ≡ monad M X … … 24 24  None ⇒ λeq_m.? 25 25 ] (refl …). elim (absurd … eq_m prf) qed. 26 27 (* playground for notation problems *)28 29 inductive option_bis (X : Type[0]) : Type[0] ≝30  Some' : X → option_bis X31  None' : option_bis X.32 33 definition option_to_option' ≝ λX.λm : option X. match m with [ Some x ⇒ Some' ? x  None ⇒ None' ?].34 35 coercion o_to_o' : ∀X.∀m : option X. option_bis X ≝ option_to_option'36 on _m : option ? to option_bis ?.37 38 39 definition Option_bis ≝ MakeMonad (mk_MonadDefinition40 option_bis41 (λX.Some' X)42 (λX,Y,m,f.match m with [Some' x ⇒ f x  None' ⇒ None' ?])43 ???). //44 #X[#Y#Z] * normalize // qed.45 46 unification hint 0 ≔ X ;47 M ≟ m_def Option_bis48 (**) ⊢49 option_bis X ≡ monad M X50 .51 52 (* does not typecheck53 check (λX.λm : option_bis X.λn : option X.! x ← n ; m)54 *)
Note: See TracChangeset
for help on using the changeset viewer.