Changeset 1489


Ignore:
Timestamp:
Nov 4, 2011, 12:39:56 PM (8 years ago)
Author:
campbell
Message:

Fix up a couple of lemmas affected by the change to add_with_carries.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/Clight/casts.ma

    r961 r1489  
    4141// qed.
    4242
     43(* add_with_carries was changed to make it whd nicely in some places, but we
     44   want to undo that for some lemmas. *)
     45lemma bool_eta : ∀A:Type[0].∀b. ∀P:bool → A. if b then P true else P false = P b.
     46#A * // qed.
     47
    4348lemma add_with_carries_extend : ∀n,hx,hy,x,y,c.
    4449  (let 〈rs,cs〉 ≝ add_with_carries (S n) (hx:::x) (hy:::y) c
     
    4954<add_with_carries_unfold
    5055cases (add_with_carries n x y c)
    51 //
     56#rs' #cs' whd in ⊢ (??(match % with [ _ ⇒ ? ])?) >bool_eta //
    5257qed.
    5358
     
    166171  <add_with_carries_unfold
    167172  cases (add_with_carries n x y c)
     173  #lb #cs whd in ⊢ (??%%) >bool_eta
    168174  //
    169175| *: skip
Note: See TracChangeset for help on using the changeset viewer.