Changeset 1640 for src/common/AST.ma
 Timestamp:
 Jan 11, 2012, 5:41:45 PM (10 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/common/AST.ma
r1516 r1640 196 196 197 197 lemma typesize_pos: ∀ty. typesize ty > 0. 198 *; try *; try * /2 / qed.198 *; try *; try * /2 by le_n/ qed. 199 199 200 200 lemma typ_eq: ∀t1,t2: typ. (t1=t2) + (t1≠t2). … … 343 343 definition map_partial : ∀A,B,C:Type[0]. (B → res C) → 344 344 list (A × B) → res (list (A × C)) ≝ 345 λA,B,C,f. m map?? (λab. let 〈a,b〉 ≝ ab in do c ← f b; OK ? 〈a,c〉).345 λA,B,C,f. m_mmap ??? (λab. let 〈a,b〉 ≝ ab in do c ← f b; OK ? 〈a,c〉). 346 346 347 347 lemma map_partial_preserves_first:
Note: See TracChangeset
for help on using the changeset viewer.