Ignore:
Timestamp:
Jan 17, 2012, 1:13:08 PM (8 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/lists.ma

    r1631 r1647  
    5757] H.
    5858
     59include "utilities/monad.ma".
     60
     61definition Append : ∀A.Aop ? (nil A) ≝ λA.mk_Aop ? ? (append ?) ? ? ?.
     62// qed.
     63
     64definition List ≝ MakeMonadProps
     65  list
     66  (λX,x.[x])
     67  (λX,Y,l,f.\fold [append ?, [ ]]_{x ∈ l} (f x))
     68  ???. normalize
     69[ / by /
     70| #X#m elim m normalize //
     71| #X#Y#Z #m #f#g
     72  elim m normalize [//]
     73  #x#l' #Hi
     74  <(fold_sum ?? (f x) ? [ ] (Append ?))
     75  >Hi //
     76] qed.
     77
     78unification hint 0 ≔ X ;
     79N ≟ max_def List, M ≟ m_def N
     80(*---------------------------*)⊢
     81list X ≡ monad M X.
Note: See TracChangeset for help on using the changeset viewer.