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

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/utilities/bindLists.ma
r1636 r1647 78 78 @{ 'tnews $ts (λ${ident l} : $ty.$f) }. 79 79 80 notation > "νν ident l ×n opt('with' ident EQ) 'in' f" with precedence 47 for80 notation > "νν ident l ^ n opt('with' ident EQ) 'in' f" with precedence 47 for 81 81 ${default 82 82 @{ 'sunews $n (λ${ident l}.λ${ident EQ}.$f) } … … 84 84 }. 85 85 86 notation > "νν ident l : ty ×n opt('with' ident EQ) 'in' f" with precedence 47 for86 notation > "νν ident l : ty ^ n opt('with' ident EQ) 'in' f" with precedence 47 for 87 87 ${default 88 88 @{ 'sunews $n (λ${ident l}:$ty.λ${ident EQ}.$f) } … … 90 90 }. 91 91 92 notation < "hvbox(νν \nbsp ident l : ty ×n \nbsp 'with' \nbsp ident EQ : tyeq \nbsp 'in' \nbsp break f)" with precedence 47 for92 notation < "hvbox(νν \nbsp ident l : ty ^ n \nbsp 'with' \nbsp ident EQ : tyeq \nbsp 'in' \nbsp break f)" with precedence 47 for 93 93 @{ 'sunews $n (λ${ident l} : $ty.λ${ident EQ} : $tyeq.$f) }. 94 notation < "hvbox(νν_ n \nbsp ident l : ty ×n \nbsp 'in' \nbsp break f)" with precedence 47 for94 notation < "hvbox(νν_ n \nbsp ident l : ty ^ n \nbsp 'in' \nbsp break f)" with precedence 47 for 95 95 @{ 'unews $n (λ${ident l} : $ty.$f) }. 96 96 … … 112 112 113 113 114 coercion blist_from_list nocomposites:114 coercion blist_from_list : 115 115 ∀B,T,E. ∀l:list E. bind_list B T E ≝ blist_of_list on _l : list ? to bind_list ???. 116 116 … … 154 154 155 155 definition BindList ≝ 156 λB,T.MakeMonad (mk_MonadDefinition156 λB,T.MakeMonadProps 157 157 (* the monad *) 158 158 (λX.bind_list B T X) … … 161 161 (* bind *) 162 162 (bbind B T) 163 ???). 164 [(* bind_bind *) 163 ???. 164 [(* ret_bind *) 165 #X#Y#x#f normalize @bappend_bnil 166 (* bind_ret *) 167 #X#m elim m normalize /2 by / 168 #t #l' #Hi @bnew_proper // normalize #s#t#eq destruct @Hi 169 (* bind_bind *) 165 170 #X#Y#Z#m#f#g elim m normalize 166 171 [// … … 169 174 (* case bnew *) 170 175 #t #l #Hi @bnew_proper // 176 #x#y #x_eq_y destruct(x_eq_y) @Hi 171 177 ] 172 (* bind_ret *)173 #X#m elim m normalize /2 by /174 #t #l' #Hi @bnew_proper normalize // #s#t#eq destruct @Hi175 (* ret_bind *)176 #X#Y#x#f normalize @bappend_bnil177 178 ] 178 179 qed. 180 181 unification hint 0 ≔ B, T, X; 182 N ≟ BindList B T, M ≟ max_def N, O ≟ m_def M 183 (**) ⊢ 184 bind_list B T X ≡ monad O X. 179 185 180 186 include "utilities/state.ma". … … 195 201 theorem bcompile_append : 196 202 ∀E, R, T, U, fresh, bl1, bl2. 197 bcompile E R T U fresh (bl1 @ bl2) ≅203 (bcompile E R T U fresh (bl1 @ bl2)) ≅ 198 204 ( 199 205 ! l1 ← bcompile … fresh bl1 ;
Note: See TracChangeset
for help on using the changeset viewer.