 Timestamp:
 Nov 4, 2011, 12:39:56 PM (9 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/Clight/casts.ma
r961 r1489 41 41 // qed. 42 42 43 (* add_with_carries was changed to make it whd nicely in some places, but we 44 want to undo that for some lemmas. *) 45 lemma bool_eta : ∀A:Type[0].∀b. ∀P:bool → A. if b then P true else P false = P b. 46 #A * // qed. 47 43 48 lemma add_with_carries_extend : ∀n,hx,hy,x,y,c. 44 49 (let 〈rs,cs〉 ≝ add_with_carries (S n) (hx:::x) (hy:::y) c … … 49 54 <add_with_carries_unfold 50 55 cases (add_with_carries n x y c) 51 //56 #rs' #cs' whd in ⊢ (??(match % with [ _ ⇒ ? ])?) >bool_eta // 52 57 qed. 53 58 … … 166 171 <add_with_carries_unfold 167 172 cases (add_with_carries n x y c) 173 #lb #cs whd in ⊢ (??%%) >bool_eta 168 174 // 169 175  *: skip
Note: See TracChangeset
for help on using the changeset viewer.