Skip to content

HTTPS clone URL

Subversion checkout URL

You can clone with HTTPS or Subversion.

Download ZIP
branch: master
Fetching contributors…

Cannot retrieve contributors at this time

30 lines (25 sloc) 0.417 kb
Load "basics.tt";
Primitives;
natToInt : (x:Nat)Int;
intros;
induction x;
fill 0;
intros;
fill addInt 1 k_IH;
Qed;
ack:(x,y:Nat)<ack x y: Nat>;
intro x;
induction x;
intros;
return;
fill (S y);
intros;
induction y0;
return;
call ack k (S O);
intros;
refine k_IH;
fill call <ack (S k) k0> k_IH0;
Qed;
runack = [x,y:Int](natToInt (call <ack (intToNat x) (intToNat y)>
(ack (intToNat x) (intToNat y))));
Jump to Line
Something went wrong with that request. Please try again.