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

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/utilities/lists.ma
r1631 r1647 57 57 ] H. 58 58 59 include "utilities/monad.ma". 60 61 definition Append : ∀A.Aop ? (nil A) ≝ λA.mk_Aop ? ? (append ?) ? ? ?. 62 // qed. 63 64 definition 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 78 unification hint 0 ≔ X ; 79 N ≟ max_def List, M ≟ m_def N 80 (**)⊢ 81 list X ≡ monad M X.
Note: See TracChangeset
for help on using the changeset viewer.