define plus using nat_rec

22-180001.v

Definition Plus: nat -> nat -> nat.
  intros x.
  elim x using nat_rec.
  - intros y. apply y.
  - intros x' plus_x' y. apply (S (plus_x' y)).
Defined.

Print Plus.
(* Plus =  *)
(* fun x : nat => *)
(* nat_rec (fun _ : nat => nat -> nat) (fun y : nat => y) *)
(*   (fun (_ : nat) (plus_x' : nat -> nat) (y : nat) => S (plus_x' y)) x *)
(*      : nat -> nat -> nat *)

Print nat_rec.
(* nat_rec =  *)
(* fun P : nat -> Set => nat_rect P *)
(*      : forall P : nat -> Set, *)
(*        P 0 -> (forall n : nat, P n -> P (S n)) -> forall n : nat, P n *)

Eval compute in Plus 0 1.
Eval compute in Plus 1 1.
Eval compute in Plus 2 0.
Eval compute in Plus 10 3.