Changeset 2028 for src/ASM/Arithmetic.ma


Ignore:
Timestamp:
Jun 7, 2012, 5:58:26 PM (8 years ago)
Author:
boender
Message:
  • bugfix to Assembly (forgotten sigma)
  • added add_bitvector_of_nat_plus to Arithmetic
  • insert_lookup_opt_miss to BitVectorTrie?
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Arithmetic.ma

    r1963 r2028  
    556556qed.
    557557
     558axiom add_bitvector_of_nat_plus:
     559  ∀n,p,q:nat.
     560    add n (bitvector_of_nat ? p) (bitvector_of_nat ? q) = bitvector_of_nat ? (p+q).
     561   
    558562definition sign_bit : ∀n. BitVector n → bool ≝
    559563λn,v. match v with [ VEmpty ⇒ false | VCons _ h _ ⇒ h ].
Note: See TracChangeset for help on using the changeset viewer.