# HG changeset patch
# User Adam Chlipala <adam@chlipala.net>
# Date 1350229828 14400
# Node ID 524458532b761f8866145e74b84386b4e5ab615c
# Parent  51a8472aca68ba4276f42cd056c15ceefd75dcf5
Fix a typo in new recursion combinators example

diff -r 51a8472aca68 -r 524458532b76 src/InductiveTypes.v
--- 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. *)