Ignore:
Timestamp:
Nov 9, 2010, 3:27:30 PM (9 years ago)
Author:
mulligan
Message:

Conjunction, disjunction and 'xorjunction' implemented on bitvectors.
Lots of supporting datatypes. Vectors.ma includes some diabolical
dependent type hackery due to Wilmer.

File:
1 moved

Legend:

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

    r224 r228  
    1 include "Vectors.ma".
     1include "Vector.ma".
     2include "Nat.ma".
     3include "Bool.ma".
    24
    3 include "arithmetics/nat.ma".
    4 include "basics/bool.ma".
     5ndefinition BitVector ≝ λn: Nat. Vector Bool n.
    56
    6 ndefinition BitVector ≝ λn: nat. Vector bool n.
    7 
     7ndefinition zero ≝
     8  λn: Nat.
     9    replicate Bool n False.
     10   
    811ndefinition conjunction ≝
    9   λn: nat.
    10   λv, q: BitVector n.
    11     fold_right ∧ true v q.
     12  λn: Nat.
     13  λb: BitVector n.
     14  λc: BitVector n.
     15    zip Bool Bool Bool n conjunction b c.
     16   
     17ndefinition inclusive_disjunction ≝
     18  λn: Nat.
     19  λb: BitVector n.
     20  λc: BitVector n.
     21    zip Bool Bool Bool n inclusive_disjunction b c.
     22   
     23ndefinition exclusive_disjunction ≝
     24  λn: Nat.
     25  λb: BitVector n.
     26  λc: BitVector n.
     27    zip Bool Bool Bool n exclusive_disjunction b c.
     28   
     29   
Note: See TracChangeset for help on using the changeset viewer.