Ignore:
Timestamp:
Nov 28, 2012, 5:57:38 PM (7 years ago)
Author:
garnier
Message:

Continuing work on simulation in Clight/Cminor?

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/frontend_misc.ma

    r2496 r2500  
    130130#A #x #y * normalize
    131131#H destruct @conj @refl
     132qed.
     133
     134lemma opt_to_res_inversion :
     135  ∀A:Type[0]. ∀errmsg. ∀opt. ∀val. opt_to_res A errmsg opt = OK ? val →
     136  opt = Some ? val.
     137#A #errmsg *
     138[ 1: #val normalize #Habsurd destruct
     139| 2: #res #val normalize #Heq destruct @refl ]
    132140qed.
    133141
Note: See TracChangeset for help on using the changeset viewer.