Changeset 2453 for src/common/Errors.ma


Ignore:
Timestamp:
Nov 12, 2012, 4:30:03 PM (8 years ago)
Author:
tranquil
Message:

come changes in monad notation to

  • avoid pretty printed monsters
  • avoid "»=" notation for bind that breaks stuff like «?, ?» = ?
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/Errors.ma

    r2439 r2453  
    8989lemma bind_inversion:
    9090  ∀A,B: Type[0]. ∀f: res A. ∀g: A → res B. ∀y: B.
    91   (f »= g = return y) →
     91  (! x ← f ; g x = return y) →
    9292  ∃x. (f = return x) ∧ (g x = return y).
    9393#A #B #f #g #y cases f normalize
Note: See TracChangeset for help on using the changeset viewer.