Mercurial > cpdt > repo
comparison src/Coinductive.v @ 302:7b38729be069
Tweak mark-up to support coqdoc 8.3
author | Adam Chlipala <adam@chlipala.net> |
---|---|
date | Mon, 17 Jan 2011 15:12:30 -0500 |
parents | 2c88fc1dbe33 |
children | d5787b70cf48 |
comparison
equal
deleted
inserted
replaced
301:f4768d5a75eb | 302:7b38729be069 |
---|---|
75 | 75 |
76 Eval simpl in approx zeroes 10. | 76 Eval simpl in approx zeroes 10. |
77 (** %\vspace{-.15in}% [[ | 77 (** %\vspace{-.15in}% [[ |
78 = 0 :: 0 :: 0 :: 0 :: 0 :: 0 :: 0 :: 0 :: 0 :: 0 :: nil | 78 = 0 :: 0 :: 0 :: 0 :: 0 :: 0 :: 0 :: 0 :: 0 :: 0 :: nil |
79 : list nat | 79 : list nat |
80 ]] *) | 80 ]] |
81 *) | |
81 | 82 |
82 Eval simpl in approx trues 10. | 83 Eval simpl in approx trues 10. |
83 (** %\vspace{-.15in}% [[ | 84 (** %\vspace{-.15in}% [[ |
84 = true | 85 = true |
85 :: false | 86 :: false |
322 Theorem ones_eq' : stream_eq ones ones'. | 323 Theorem ones_eq' : stream_eq ones ones'. |
323 cofix; crush. | 324 cofix; crush. |
324 (** [[ | 325 (** [[ |
325 Guarded. | 326 Guarded. |
326 | 327 |
327 ]] *) | 328 ]] |
329 *) | |
328 Abort. | 330 Abort. |
329 (* end thide *) | 331 (* end thide *) |
330 | 332 |
331 (** The standard [auto] machinery sees that our goal matches an assumption and so applies that assumption, even though this violates guardedness. One usually starts a proof like this by [destruct]ing some parameter and running a custom tactic to figure out the first proof rule to apply for each case. Alternatively, there are tricks that can be played with %``%#"#hiding#"#%''% the co-inductive hypothesis. *) | 333 (** The standard [auto] machinery sees that our goal matches an assumption and so applies that assumption, even though this violates guardedness. One usually starts a proof like this by [destruct]ing some parameter and running a custom tactic to figure out the first proof rule to apply for each case. Alternatively, there are tricks that can be played with %``%#"#hiding#"#%''% the co-inductive hypothesis. *) |
332 | 334 |