Changeset 2444 for src/common/IOMonad.ma


Ignore:
Timestamp:
Nov 8, 2012, 6:47:04 PM (7 years ago)
Author:
campbell
Message:

Some inversion lemmas for after_n_steps for dealing with >1 source steps.
Also, a few more coercions for IO/error equations when the type isn't
reduced.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/IOMonad.ma

    r2428 r2444  
    426426  on _E:eq (IO ???) ?? to eq (res ?) ??.
    427427
     428(* and for an unreduced form *)
     429coercion io_monad_eq_from_res :
     430  ∀O,I,T,e,v. ∀E:err_to_io O I T e = Value O I T v. e = OK T v ≝ io_eq_to_res
     431  on _E:eq (monad (max_def (IOMonad ??)) ?) ?? to eq (res ?) ??.
     432
    428433(* Similarly for opt *)
    429434
     
    441446  on _E:eq (IO ???) ?? to eq (option ?) ??.
    442447
    443 
    444 
     448coercion io_monad_eq_from_opt :
     449  ∀O,I,T,e,m,v. ∀E:opt_to_io O I T m e = Value O I T v. e = Some T v ≝ io_eq_to_opt
     450  on _E:eq (monad (max_def (IOMonad ??)) ?) ?? to eq (option ?) ??.
     451
     452
     453
Note: See TracChangeset for help on using the changeset viewer.