Mercurial > cpdt > repo
comparison src/InductiveTypes.v @ 568:81d63d9c1cc5
Port to Coq 8.9.0
| author | Adam Chlipala <adam@chlipala.net> |
|---|---|
| date | Sun, 20 Jan 2019 15:16:29 -0500 |
| parents | 429e95d23b26 |
| children | 1dc1d41620b6 |
comparison
equal
deleted
inserted
replaced
| 567:ec0ce5129fc4 | 568:81d63d9c1cc5 |
|---|---|
| 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 Implicit 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 [Implicit Arguments]%~\index{Vernacular commands!Implicit 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}% [[ |
| 488 Inductive list (T : Set) : Set := | 488 Inductive list (T : Set) : Set := |
| 489 Nil : list T | Cons : T -> list T -> list T | 489 Nil : list T | Cons : T -> list T -> list T |