Changeset 2453 for src/common/IOMonad.ma


Ignore:
Timestamp:
Nov 12, 2012, 4:30:03 PM (7 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/IOMonad.ma

    r2444 r2453  
    369369lemma bind_res_value : ∀O,I,A,B,e,f,v. ∀P:B → Type[0].
    370370  (∀a. e = OK A a → f a = OK B v → P v) →
    371   (match e »= f with [ OK v ⇒ Value … v | Error m ⇒ Wrong … m ] = Value O I B v → P v).
     371  (match m_bind … e f with [ OK v ⇒ Value … v | Error m ⇒ Wrong … m ] = Value O I B v → P v).
    372372#O #I #A #B *
    373373[ #a #f #v #P #H #E @H [ @a | @refl | normalize in E; cases (f a) in E ⊢ %;
     
    403403lemma bindIO_inversion: ∀O,I.
    404404  ∀A,B: Type[0]. ∀f: IO O I A. ∀g: A → IO O I B. ∀y: B.
    405   (f »= g = return y) →
     405  (m_bind … f g = return y) →
    406406  ∃x. (f = return x) ∧ (g x = return y).
    407407#O #I #A #B #f #g #y cases f normalize
Note: See TracChangeset for help on using the changeset viewer.