Changeset 2496 for src/Clight/frontend_misc.ma
 Timestamp:
 Nov 27, 2012, 5:50:51 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/Clight/frontend_misc.ma
r2468 r2496 85 85 ∃x. e = Some ? x ∧ f x = Some ? res. 86 86 #A #B #e #res #f cases e normalize nodelta 87 [ 1: #Habsurd destruct (Habsurd) 88  2: #a #Heq %{a} @conj >Heq @refl ] 89 qed. 90 91 lemma res_inversion : 92 ∀A,B:Type[0]. 93 ∀e:option A. 94 ∀errmsg. 95 ∀result:B. 96 ∀f:A → res B. 97 match e with 98 [ None ⇒ Error ? errmsg 99  Some x ⇒ f x ] = OK ? result → 100 ∃x. e = Some ? x ∧ f x = OK ? result. 101 #A #B #e #errmsg #result #f cases e normalize nodelta 87 102 [ 1: #Habsurd destruct (Habsurd) 88 103  2: #a #Heq %{a} @conj >Heq @refl ]
Note: See TracChangeset
for help on using the changeset viewer.