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/Arithmetic.ma

    r313 r349  
    146146  nassumption;
    147147nqed.
     148
     149ndefinition full_add:
     150  ∀n: Nat.
     151  ∀b, c: BitVector n.
     152  ∀d: Bit.
     153    fold_left_i ? ? (
     154      λb1, b2: Bool.
     155      λd.
     156        let 〈c1,r〉 ≝ d in
     157          〈inclusive_disjunction (conjunction b1 b2)
     158                                 (conjunction c1 (inclusive_disjunction b1 b2)),
     159           (exclusive_disjunction (exclusive_disjunction b1 b2) c1) :: r〉)
     160             b c 〈c, [ ]〉.
     161   
     162    (fun b1 b2 (c,r) -> b1 & b2 || c & (b1 || b2),xor (xor b1 b2) c::r) l r (c,[])
     163   
     164ndefinition half_add ≝
     165  λn: Nat.
     166  λb, c: BitVector n.
     167    full_add n b c false.
     168
Note: See TracChangeset for help on using the changeset viewer.