Changeset 868 for src/ASM/BitVector.ma


Ignore:
Timestamp:
May 31, 2011, 5:28:12 PM (9 years ago)
Author:
mulligan
Message:

more changes

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/BitVector.ma

    r744 r868  
    9191(* -=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-=-= *)
    9292
     93definition eq_b ≝
     94  λb, c: bool.
     95    if b then
     96      c
     97    else
     98      notb c.
     99
    93100definition eq_bv ≝
    94101  λn: nat.
    95102  λb, c: BitVector n.
    96     eq_v bool n (λd, e.
    97       if (d ∧ e) ∨ ((¬d) ∧ (¬e)) then
    98         true
    99       else
    100         false) b c.
     103    eq_v bool n eq_b b c.
    101104
    102105lemma eq_bv_elim: ∀P:bool → Type[0]. ∀n. ∀x,y.
Note: See TracChangeset for help on using the changeset viewer.