Mercurial > cpdt > repo
comparison src/InductiveTypes.v @ 574:1dc1d41620b6
Builds with Coq 8.15.2
| author | Adam Chlipala <adam@chlipala.net> |
|---|---|
| date | Sun, 31 Jul 2022 14:48:22 -0400 |
| parents | 81d63d9c1cc5 |
| children |
comparison
equal
deleted
inserted
replaced
| 573:c3d77f2bb92c | 574:1dc1d41620b6 |
|---|---|
| 477 induction ls1; crush. | 477 induction ls1; crush. |
| 478 Qed. | 478 Qed. |
| 479 (* end thide *) | 479 (* end thide *) |
| 480 End list. | 480 End list. |
| 481 | 481 |
| 482 Arguments Nil [T]. | 482 Arguments Nil {T}. |
| 483 | 483 |
| 484 (** After we end the section, the [Variable]s we used are added as extra function parameters for each defined identifier, as needed. With an [Arguments]%~\index{Vernacular commands!Arguments}% command, we ask that [T] be inferred when we use [Nil]; Coq's heuristics already decided to apply a similar policy to [Cons], because of the [Set Implicit Arguments]%~\index{Vernacular commands!Set Implicit Arguments}% command elided at the beginning of this chapter. We verify that our definitions have been saved properly using the [Print] command, a cousin of [Check] which shows the definition of a symbol, rather than just its type. *) | 484 (** After we end the section, the [Variable]s we used are added as extra function parameters for each defined identifier, as needed. With an [Arguments]%~\index{Vernacular commands!Arguments}% command, we ask that [T] be inferred when we use [Nil]; Coq's heuristics already decided to apply a similar policy to [Cons], because of the [Set Implicit Arguments]%~\index{Vernacular commands!Set Implicit Arguments}% command elided at the beginning of this chapter. We verify that our definitions have been saved properly using the [Print] command, a cousin of [Check] which shows the definition of a symbol, rather than just its type. *) |
| 485 | 485 |
| 486 Print list. | 486 Print list. |
| 487 (** %\vspace{-.15in}% [[ | 487 (** %\vspace{-.15in}% [[ |