Mercurial > cpdt > repo

comparison src/InductiveTypes.v @ 302:7b38729be069

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
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
50 induction x. 50 induction x.
51 51
52 (** The goal changes to: 52 (** The goal changes to:
53 [[ 53 [[
54 tt = tt 54 tt = tt
55 ]] *) 55 ]]
56 *)
56 57
57 (** ...which we can discharge trivially. *) 58 (** ...which we can discharge trivially. *)
58 59
59 reflexivity. 60 reflexivity.
60 Qed. 61 Qed.
368 : forall P : nat_btree -> Prop, 369 : forall P : nat_btree -> Prop,
369 P NLeaf -> 370 P NLeaf ->
370 (forall n : nat_btree, 371 (forall n : nat_btree,
371 P n -> forall (n0 : nat) (n1 : nat_btree), P n1 -> P (NNode n n0 n1)) -> 372 P n -> forall (n0 : nat) (n1 : nat_btree), P n1 -> P (NNode n n0 n1)) ->
372 forall n : nat_btree, P n 373 forall n : nat_btree, P n
373 ]] *) 374 ]]
375 *)
374 376
375 377
376 (** * Parameterized Types *) 378 (** * Parameterized Types *)
377 379
378 (** We can also define polymorphic inductive types, as with algebraic datatypes in Haskell and ML. *) 380 (** We can also define polymorphic inductive types, as with algebraic datatypes in Haskell and ML. *)
893 Locate "/\". 895 Locate "/\".
894 (** %\vspace{-.15in}% [[ 896 (** %\vspace{-.15in}% [[
895 Notation Scope 897 Notation Scope
896 "A /\ B" := and A B : type_scope 898 "A /\ B" := and A B : type_scope
897 (default interpretation) 899 (default interpretation)
898 ]] *) 900 ]]
901 *)
899 902
900 Print and. 903 Print and.
901 (** %\vspace{-.15in}% [[ 904 (** %\vspace{-.15in}% [[
902 Inductive and (A : Prop) (B : Prop) : Prop := conj : A -> B -> A /\ B 905 Inductive and (A : Prop) (B : Prop) : Prop := conj : A -> B -> A /\ B
903 For conj: Arguments A, B are implicit 906 For conj: Arguments A, B are implicit
1100 (** [[ 1103 (** [[
1101 H : true = false 1104 H : true = false
1102 ============================ 1105 ============================
1103 True 1106 True
1104 1107
1105 ]] *) 1108 ]]
1109 *)
1106 1110
1107 trivial. 1111 trivial.
1108 Qed. 1112 Qed.
1109 (* end thide *) 1113 (* end thide *)
1110 1114