Ignore:
Timestamp:
Nov 26, 2010, 6:13:26 PM (9 years ago)
Author:
mulligan
Message:

Added fold_right_i, equivalent of O'Caml's fold_right2.

File:
1 edited

Legend:

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

    r315 r320  
    228228    ].
    229229   
    230 naxiom half_add:
    231   ∀n: Nat.
    232   ∀b, c: BitVector n.
    233     Bool × (BitVector n).
    234    
    235230naxiom full_add:
    236231  ∀n: Nat.
     
    238233  ∀d: Bit.
    239234    Bool × (BitVector n).
     235   
     236ndefinition half_add ≝
     237  λn: Nat.
     238  λb, c: BitVector n.
     239    full_add n b c false.
Note: See TracChangeset for help on using the changeset viewer.