Changeset 2500 for src/common


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/common/Errors.ma

    r2496 r2500  
    273273  ∀A,B,C: Type[0]. ∀f: res (A×B). ∀g: ∀a:A.∀b:B. f = OK ? 〈a,b〉 → res C. ∀z.
    274274  bind2_eq ??? f g = return z →
    275   ∃x. ∃y. ∃Eq. f = return 〈x, y〉 ∧ g x y Eq = return z.
     275  ∃x. ∃y. ∃Eq. g x y Eq = return z.
    276276#A #B #C #f cases f
    277 [ * #a #b #g normalize #z #Heq %{a} %{b} %{(refl ??)} @conj try @refl @Heq
     277[ * #a #b #g normalize #z #Heq %{a} %{b} %{(refl ? (OK ? 〈a,b〉))} @Heq
    278278| #errmsg #g #z normalize #Habsurd destruct (Habsurd) ]
    279 qed. 
     279qed.
    280280
    281281definition res_to_opt : ∀A:Type[0]. res A → option A ≝
Note: See TracChangeset for help on using the changeset viewer.