Mercurial > cpdt > repo

comparison src/Coinductive.v @ 348:f3154417cd41

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Typo fix in template comment
author Adam Chlipala <adam@chlipala.net>
date Tue, 25 Oct 2011 10:51:31 -0400
parents 36a08cad9245
children de7db21a016c
comparison
equal deleted inserted replaced
347:36a08cad9245 348:f3154417cd41
64 with falses_trues : stream bool := Cons false trues_falses. 64 with falses_trues : stream bool := Cons false trues_falses.
65 (* end thide *) 65 (* end thide *)
66 66
67 (** Co-inductive values are fair game as arguments to recursive functions, and we can use that fact to write a function to take a finite approximation of a stream. *) 67 (** Co-inductive values are fair game as arguments to recursive functions, and we can use that fact to write a function to take a finite approximation of a stream. *)
68 68
69 (* EX: Defint a function to calculate a finite approximation of a stream, to a particular length. *) 69 (* EX: Define a function to calculate a finite approximation of a stream, to a particular length. *)
70 (* begin thide *) 70 (* begin thide *)
71 71
72 Fixpoint approx A (s : stream A) (n : nat) : list A := 72 Fixpoint approx A (s : stream A) (n : nat) : list A :=
73 match n with 73 match n with
74 | O => nil 74 | O => nil