Permalink
Find file
Fetching contributors…
Cannot retrieve contributors at this time
66 lines (54 sloc) 890 Bytes
Data Nat:* = O:Nat | S:(k:Nat)Nat;
plus : (m:Nat)(n:Nat)Nat;
intro m;
induction m;
intros;
fill n;
intros;
refine S;
fill k_IH n0;
Qed;
adderType : (m:Nat)(n:Nat)*;
intros;
induction m;
fill Nat;
intros;
fill (n:Nat)k_IH;
Qed;
adder: (m:Nat)(n:Nat)(adderType m n);
intro m;
induction m;
intros;
fill n;
intros;
compute;
intros;
fill k_IH (plus n0 n1);
Qed;
mult:(m:Nat)(n:Nat)Nat;
intros;
induction m;
fill O;
intros;
fill (plus n k_IH);
Qed;
fact:(m:Nat)Nat;
intros;
induction m;
fill (S O);
intros;
fill (mult (S k) k_IH);
Qed;
testval = fact (S (S (S (S (S (S (S (S (S O)))))))));
Data Vect (A:*):(n:Nat)*
= vnil:Vect A O
| vcons:(k:Nat)(x:A)(xs:Vect A k)Vect A (S k);
vectsum : (k:Nat)(v:Vect Nat k)Nat;
intros;
induction v;
fill O;
intros;
fill (plus x xs_IH);
Qed;
testvect2 = vcons _ _ (S O) (vcons _ _ (S (S (S O))) (vnil Nat));
testval2 = vectsum _ testvect2;