(* Solution to Assignment 11: Primitive Recursion and T *)
Set Implicit Arguments.
Tactic Notation "inv" hyp(A)  := inversion A ; subst ; clear A.

Fixpoint primrec (X : Type) (n : nat) (x : X) (f : nat -> X -> X) : X :=
match n with
| O => x
| S n' => f n' (primrec n' x f)
end.

(*** Exercise ***)
(*
Definition T_add : nat -> nat -> nat := ...

Compute T_add 2 3.
Compute T_add 4 2.
*)

(*** Exercise: Define the abstract syntax and a small-step semantics for T ***)