Ignore:
Timestamp:
Dec 1, 2010, 11:18:05 AM (9 years ago)
Author:
mulligan
Message:

Added fold_right_i (with dependent type) to List file.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D4.1/Matita/BitVector.ma

    r343 r349  
    217217        ((exponential (S (S Z)) o) * hdval) + nat_of_bitvector o tl
    218218    ].
    219    
    220 naxiom full_add:
    221   ∀n: Nat.
    222   ∀b, c: BitVector n.
    223   ∀d: Bit.
    224     Bool × (BitVector n).
    225    
    226 ndefinition half_add ≝
    227   λn: Nat.
    228   λb, c: BitVector n.
    229     full_add n b c false.
Note: See TracChangeset for help on using the changeset viewer.