Mercurial > cpdt > repo
changeset 472:524458532b76
Fix a typo in new recursion combinators example
| author | Adam Chlipala <adam@chlipala.net> |
|---|---|
| date | Sun, 14 Oct 2012 11:50:28 -0400 |
| parents | 51a8472aca68 |
| children | 39c204d2262c |
| files | src/InductiveTypes.v |
| diffstat | 1 files changed, 5 insertions(+), 1 deletions(-) [+] |
line wrap: on
line diff
--- a/src/InductiveTypes.v Mon Oct 08 16:04:49 2012 -0400 +++ b/src/InductiveTypes.v Sun Oct 14 11:50:28 2012 -0400 @@ -780,7 +780,11 @@ end. Definition plus_rec : nat -> nat -> nat := - nat_rec (fun _ : nat => nat -> nat) (fun _ => O) (fun _ r m => S (r m)). + nat_rec (fun _ : nat => nat -> nat) (fun m => m) (fun _ r m => S (r m)). + +Theorem plus_equivalent : plus_recursive = plus_rec. + reflexivity. +Qed. (** Going even further down the rabbit hole, [nat_rect] itself is not even a primitive. It is a functional program that we can write manually. *)