ivor-0.1.5: examplett/ack.tt

Load "nat.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))));

Eval runack 2 6; {- 15 -}
Eval runack 3 4; {- 125 -}
Eval runack 3 5; {- 253 -}

Eval runack 4 4; {- no chance -}