Changeset 2453 for src/common


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 «?, ?» = ?
Location:
src/common
Files:
3 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
  • 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
  • src/common/PositiveMap.ma

    r2439 r2453  
    425425match b with
    426426[ pm_leaf ⇒ pm_leaf ?
    427 | pm_node a l r ⇒ pm_node ? (a »= f)
     427| pm_node a l r ⇒ pm_node ? (!x ← a ; f x)
    428428    (map_opt ?? f l)
    429429    (map_opt ?? f r)
Note: See TracChangeset for help on using the changeset viewer.