Changeset 1640 for src/common/AST.ma


Ignore:
Timestamp:
Jan 11, 2012, 5:41:45 PM (9 years ago)
Author:
tranquil
Message:
  • finished fork of semantics.ma
  • unification of Errors under the monad notations brings problems in type checking when res and IO are used together. Needs a lot of annotations, and may break the pre-fork material
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/AST.ma

    r1516 r1640  
    196196
    197197lemma typesize_pos: ∀ty. typesize ty > 0.
    198 *; try *; try * /2/ qed.
     198*; try *; try * /2 by le_n/ qed.
    199199
    200200lemma typ_eq: ∀t1,t2: typ. (t1=t2) + (t1≠t2).
     
    343343definition map_partial : ∀A,B,C:Type[0]. (B → res C) →
    344344                         list (A × B) → res (list (A × C)) ≝
    345 λA,B,C,f. mmap ?? (λ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〉).
    346346
    347347lemma map_partial_preserves_first:
Note: See TracChangeset for help on using the changeset viewer.