A direct definition of addition
Give another definition of addition on
nat
, without using
Fixpoint
nor
fix
, but as an application of
nat_rec
.
Is your definition equivalent to
Coq
's
plus
?
Solution
Look at
this file
Going home
Pierre Castéran