 Timestamp:
 Oct 20, 2011, 2:08:39 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ASM/Arithmetic.ma
r1404 r1426 140 140 definition nat_of_bitvector : ∀n:nat. BitVector n → nat ≝ 141 141 λn,v. nat_of_bitvector_aux n O v. 142 143 axiom bitvector_of_nat_ok: 144 ∀n,x,y.bitvector_of_nat (S n) x = bitvector_of_nat (S n) y → x = y. 145 (* if anyone wants to prove this... *) 146 142 147 143 definition two_complement_negation ≝ 148 144 λn: nat.
Note: See TracChangeset
for help on using the changeset viewer.