Ignore:
Timestamp:
Nov 8, 2010, 5:04:27 PM (9 years ago)
Author:
mulligan
Message:

Changes to bit vectors and vectors.

File:
1 edited

Legend:

Unmodified
Added
Removed

  • Deliverables/D4.1/Matita/BitVectors.ma

    r223 r224  
     1include "Vectors.ma".
     2
     3include "arithmetics/nat.ma".
     4include "basics/bool.ma".
     5
     6ndefinition BitVector ≝ λn: nat. Vector bool n.
     7
     8ndefinition conjunction ≝
     9  λn: nat.
     10  λv, q: BitVector n.
     11    fold_right ∧ true v q.
Note: See TracChangeset for help on using the changeset viewer.