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. *)