Changeset 2154 for src/ASM/Arithmetic.ma


Ignore:
Timestamp:
Jul 5, 2012, 2:22:08 PM (8 years ago)
Author:
sacerdot
Message:

Code shuffled around.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Arithmetic.ma

    r2149 r2154  
    703703   nat_of_bitvector n (add n v1 v2) = nat_of_bitvector n v1 + nat_of_bitvector n v2.
    704704
     705axiom add_bitvector_of_nat:
     706 ∀n,m1,m2.
     707  bitvector_of_nat n (m1 + m2) =
     708   add n (bitvector_of_nat n m1) (bitvector_of_nat n m2).
     709
    705710example add_SO:
    706711  ∀n: nat.
Note: See TracChangeset for help on using the changeset viewer.