Mercurial > cpdt > repo

comparison src/InductiveTypes.v @ 472:524458532b76

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
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 1fd4109f7b31
comparison
equal deleted inserted replaced
471:51a8472aca68 472:524458532b76
778 | O => fun m => m 778 | O => fun m => m
779 | S n' => fun m => S (plus_recursive n' m) 779 | S n' => fun m => S (plus_recursive n' m)
780 end. 780 end.
781 781
782 Definition plus_rec : nat -> nat -> nat := 782 Definition plus_rec : nat -> nat -> nat :=
783 nat_rec (fun _ : nat => nat -> nat) (fun _ => O) (fun _ r m => S (r m)). 783 nat_rec (fun _ : nat => nat -> nat) (fun m => m) (fun _ r m => S (r m)).
784
785 Theorem plus_equivalent : plus_recursive = plus_rec.
786 reflexivity.
787 Qed.
784 788
785 (** 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. *) 789 (** 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. *)
786 790
787 Print nat_rect. 791 Print nat_rect.
788 (** %\vspace{-.15in}%[[ 792 (** %\vspace{-.15in}%[[