user:
Here are the definition of nat in lean 4 and add_left in lean 4:
inductive u_nat : Type | zero : u_nat | succ : u_nat → u_nat def add_left : u_nat → u_nat → u_nat | u_nat.zero, n => n | u_nat.succ n', n => u_nat.succ (add_left n' n)
Using that, give me the definition of add_right by recursing on the right.
morph-prover-v0:
Here is a Lean 4 code snippet that defines add_right using pattern matching and recursion:
inductive u_nat : Type | zero : u_nat | succ : u_nat → u_nat def add_left : u_nat → u_nat → u_nat | u_nat.zero, n => n | u_nat.succ n', n => u_nat.succ (add_left n' n) def add_right : u_nat → u_nat → u_nat | m, u_nat.zero => m | m, u_nat.succ n => u_nat.succ (add_right m n)
This code defines u_nat as an inductive type representing natural numbers, and add_left as a function that adds a constant to the left of a u_nat. The add_right function is defined by recursion on the right argument.