Changeset 224 for Deliverables
 Timestamp:
 Nov 8, 2010, 5:04:27 PM (10 years ago)
 Location:
 Deliverables/D4.1/Matita
 Files:

 2 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D4.1/Matita/BitVectors.ma
r223 r224 1 include "Vectors.ma". 2 3 include "arithmetics/nat.ma". 4 include "basics/bool.ma". 5 6 ndefinition BitVector ≝ λn: nat. Vector bool n. 7 8 ndefinition conjunction ≝ 9 λn: nat. 10 λv, q: BitVector n. 11 fold_right ∧ true v q. 
Deliverables/D4.1/Matita/Vectors.ma
r223 r224 2 2 (* Vectors.ma: Fixed length bitvectors, and routine operations on them. *) 3 3 (* ===================================== *) 4 5 include "Cartesian.ma". 6 include "List.ma". 4 7 5 8 include "logic/pts.ma". … … 12 15 ninductive Vector (A: Type[0]): nat → Type[0] ≝ 13 16 Empty: Vector A 0 14  Cons: ∀n: nat. A → Vector A n → Vector A ( n + 1).17  Cons: ∀n: nat. A → Vector A n → Vector A (S n). 15 18 16 19 nlet rec map (A: Type[0]) (B: Type[0]) (n: nat) (f: A → B) (v: Vector A n) on v ≝ … … 37 40 match v with 38 41 [ Empty ⇒ 0 39  Cons n hd tl ⇒ 1 + length A n tl42  Cons n hd tl ⇒ S (length A n tl) 40 43 ]. 41 42 (* 43 nlet rec append (A: Type[0]) (n: nat) (m: nat) 44 (v: Vector A n) (q: Vector A m) on v ≝ 45 match v with 46 [ Empty ⇒ q 47  Cons n hd tl ⇒ Cons ? n hd (append A n m tl q) 44 45 nlet rec from_list (A: Type[0]) (l: List A) on l ≝ 46 match l with 47 [ Empty ⇒ Empty A 48  Cons hd tl ⇒ Cons (length A tl) hd (from_list A tl) 48 49 ]. 49 *)50 51 (*52 nlet rec reverse (A: Type[0]) (n: nat) (v: Vector A n) on v ≝53 match v with54 [ Empty ⇒ Empty A55  Cons n hd tl ⇒ append56 57 nlemma length_correct:58 ∀A: Type[0].59 ∀n: nat.60 ∀v: Vector A n.61 length A n v = n.62 #A n v;63 nelim v.64 nnormalize.65 @.66 #n0 H V H.67 nnormalize.68 nrewrite > H.69 *)
Note: See TracChangeset
for help on using the changeset viewer.