Ignore:
Timestamp:
Jan 17, 2012, 1:13:08 PM (9 years ago)
Author:
tranquil
Message:
  • corrected some notation problems
  • adapted Cligth with slight modifications to new monad framework
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/utilities/option.ma

    r1640 r1647  
    22include "basics/types.ma".
    33
    4 definition Option ≝ MakeMonad (mk_MonadDefinition
     4definition Option ≝ MakeMonadProps
    55  (* the monad *)
    66  option
     
    99  (* bind *)
    1010  (λ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.
    1313
    1414include "hints_declaration.ma".
    1515unification hint 0 ≔ X;
    16 M ≟ m_def Option
     16N ≟ max_def Option, M ≟ m_def N
    1717(*---------------*) ⊢
    1818option X ≡ monad M X
     
    2424  | None ⇒ λeq_m.?
    2525  ] (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 X
    31 | 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_MonadDefinition
    40   option_bis
    41   (λ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_bis
    48 (*---------------*) ⊢
    49 option_bis X ≡ monad M X
    50 .
    51 
    52 (* does not typecheck
    53 check (λX.λm : option_bis X.λn : option X.! x ← n ; m)
    54 *)
Note: See TracChangeset for help on using the changeset viewer.