Mercurial > cpdt > repo

comparison src/InductiveTypes.v @ 210:b149a07b9b5b

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Most old Sestoft suggestions processed
author Adam Chlipala <adamc@hcoop.net>
date Mon, 09 Nov 2009 13:18:46 -0500
parents b9e9ff52913c
children c4b1c0de7af9
comparison
equal deleted inserted replaced
209:90af611e2993 210:b149a07b9b5b
435 435
436 (* begin hide *) 436 (* begin hide *)
437 Implicit Arguments Nil [T]. 437 Implicit Arguments Nil [T].
438 (* end hide *) 438 (* end hide *)
439 439
440 (** After we end the section, the [Variable]s we used are added as extra function parameters for each defined identifier, as needed. *) 440 (** After we end the section, the [Variable]s we used are added as extra function parameters for each defined identifier, as needed. We verify that this has happened using the [Print] command, a cousin of [Check] which shows the definition of a symbol, rather than just its type. *)
441 441
442 Print list. 442 Print list.
443 (** %\vspace{-.15in}% [[ 443 (** %\vspace{-.15in}% [[
444 Inductive list (T : Set) : Set := 444 Inductive list (T : Set) : Set :=
445 Nil : list T | Cons : T -> list T -> list Tlist 445 Nil : list T | Cons : T -> list T -> list Tlist