Permalink
Switch branches/tags
Nothing to show
Find file
Fetching contributors…
Cannot retrieve contributors at this time
40 lines (30 sloc) 538 Bytes
Load "nat.tt";
-- plusST = lam m,n:{{Nat}}.
-- case !m of
-- O -> n
-- S k -> {'S ~(plusST ~k n)}
plusST:(m,n:{{Nat}}){{Nat}};
intros;
induction !m;
fill n;
intros;
fill {'S ~k_IH};
Qed;
quote4 = {'plus (S (S O)) (S (S O))};
quote8 = plusST quote4 quote4;
Eval quote8;
Eval !quote8;
quotefoo = [m:Nat][n:Nat]{'plus (S (S O)) (([p:Nat](plus m p)) n)};
mult:(m,n:Nat)Nat;
intros;
induction m;
refine O;
intros;
refine (plus n k_IH);
Qed;
power:(m,x:Nat)Nat;
induction m;
fill (S O);
intros;
fill (mult x k_IH);
Qed;