Changeset 2428 for src/common/IOMonad.ma


Ignore:
Timestamp:
Nov 6, 2012, 12:02:13 PM (7 years ago)
Author:
campbell
Message:

Tighten requirements on switch statements in Clight to only give semantics
when the controlling expression's type and values match up and the cases'
labels make sense.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/IOMonad.ma

    r2145 r2428  
    426426  on _E:eq (IO ???) ?? to eq (res ?) ??.
    427427
     428(* Similarly for opt *)
     429
     430lemma io_eq_to_opt : ∀O,I. ∀T:Type[0]. ∀e:option T. ∀m,v.
     431  opt_to_io … m e = Value O I T v →
     432  e = Some T v.
     433#O #I #T *
     434[ #m #v #E normalize in E; destruct
     435| #t #m #v #E normalize in E; destruct %
     436]
     437qed.
     438
     439coercion io_eq_from_opt :
     440  ∀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
     441  on _E:eq (IO ???) ?? to eq (option ?) ??.
     442
     443
     444
Note: See TracChangeset for help on using the changeset viewer.