Mercurial > cpdt > repo
comparison src/Generic.v @ 360:e0d91bcf70ec
Pass through old content of Reflection
| author | Adam Chlipala <adam@chlipala.net> |
|---|---|
| date | Wed, 02 Nov 2011 14:48:25 -0400 |
| parents | 059c51227e69 |
| children | d1276004eec9 |
comparison
equal
deleted
inserted
replaced
| 359:059c51227e69 | 360:e0d91bcf70ec |
|---|---|
| 528 (hmake | 528 (hmake |
| 529 (fun (x : constructor) (_ : nonrecursive x) | 529 (fun (x : constructor) (_ : nonrecursive x) |
| 530 (r : ilist nat (recursive x)) => foldr plus 1%nat r) dt) v > 0". | 530 (r : ilist nat (recursive x)) => foldr plus 1%nat r) dt) v > 0". |
| 531 >> | 531 >> |
| 532 | 532 |
| 533 Matching the type of [dok] with the type of our conclusion requires more than simple first-order unification, so [apply] is not up to the challenge. We can use the [pattern] tactic to get our goal into a form that makes it apparent exactly what the induction hypothesis is. *) | 533 Matching the type of [dok] with the type of our conclusion requires more than simple first-order unification, so [apply] is not up to the challenge. We can use the %\index{tactics!pattern}%[pattern] tactic to get our goal into a form that makes it apparent exactly what the induction hypothesis is. *) |
| 534 | 534 |
| 535 pattern v. | 535 pattern v. |
| 536 (** %\vspace{-.15in}%[[ | 536 (** %\vspace{-.15in}%[[ |
| 537 ============================ | 537 ============================ |
| 538 (fun t : T => | 538 (fun t : T => |