Changeset 1946 for src/ASM/Fetch.ma


Ignore:
Timestamp:
May 15, 2012, 12:01:30 AM (8 years ago)
Author:
sacerdot
Message:

\snd half_add => add everywhere

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Fetch.ma

    r1941 r1946  
    99
    1010definition code_memory_size ≝ bitvector_max_nat 16.
    11 
    12 definition add ≝
    13   λn: nat.
    14   λl, r: BitVector n.
    15     \snd (half_add n l r).
    16 
    17 axiom add_zero:
    18   ∀n: nat.
    19   ∀l: BitVector n.
    20     l = add n l (zero …).
    21 
    22 axiom add_associative:
    23   ∀n: nat.
    24   ∀l, c, r: BitVector n.
    25     add … l (add … c r) = add … (add … l c) r.
    2611
    2712include alias "ASM/BitVectorTrie.ma".
Note: See TracChangeset for help on using the changeset viewer.