Mercurial > cpdt > repo

comparison src/Coinductive.v @ 450:f28bdd8414e0

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Proofreading pass through Chapter 5
author Adam Chlipala <adam@chlipala.net>
date Fri, 17 Aug 2012 15:16:08 -0400
parents 89c67796754e
children 51a8472aca68
comparison
equal deleted inserted replaced
449:79190c225f1a 450:f28bdd8414e0
302 302
303 It turns out that we are best served by proving an auxiliary lemma. *) 303 It turns out that we are best served by proving an auxiliary lemma. *)
304 304
305 Abort. 305 Abort.
306 306
307 (** First, we need to define a function that seems pointless on first glance. *) 307 (** First, we need to define a function that seems pointless at first glance. *)
308 308
309 Definition frob A (s : stream A) : stream A := 309 Definition frob A (s : stream A) : stream A :=
310 match s with 310 match s with
311 | Cons h t => Cons h t 311 | Cons h t => Cons h t
312 end. 312 end.