Changeset 1954 for src/common


Ignore:
Timestamp:
May 16, 2012, 2:44:05 PM (8 years ago)
Author:
campbell
Message:

Initial state is in the labelling simulation
(modulo global envs results).

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/Errors.ma

    r1949 r1954  
    232232qed.
    233233
     234lemma opt_eq_from_res : ∀T,m,e,v.
     235  opt_to_res T m e = return v →
     236  e = Some T v.
     237#T #m * [ #v #E normalize in E; destruct | #e' #v #E normalize in E; destruct % ]
     238qed.
     239
     240coercion opt_eq_from_res :
     241  ∀T,m,e,v. ∀E:opt_to_res T m e = return v. e = Some T v ≝ opt_eq_from_res
     242  on _E:eq (res ?) ?? to eq (option ?) ??.
     243
    234244(* A variation of bind and its notation that provides an equality proof for
    235245   later use. *)
Note: See TracChangeset for help on using the changeset viewer.