1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 (* This file was automatically generated: do not edit *********************)
19 (*#***********************************************************************)
21 (* v * The Coq Proof Assistant / The Coq Development Team *)
23 (* <O___,, * CNRS-Ecole Polytechnique-INRIA Futurs-Universite Paris Sud *)
25 (* \VV/ **************************************************************)
27 (* // * This file is distributed under the terms of the *)
29 (* * GNU Lesser General Public License Version 2.1 *)
31 (*#***********************************************************************)
33 (*i $Id: Datatypes.v,v 1.26.2.1 2004/07/16 19:31:03 herbelin Exp $ i*)
35 include "Init/Notations.ma".
37 include "Init/Logic.ma".
40 Set Implicit Arguments.
43 (*#* [unit] is a singleton datatype with sole inhabitant [tt] *)
45 inline procedural "cic:/Coq/Init/Datatypes/unit.ind".
47 (*#* [bool] is the datatype of the booleans values [true] and [false] *)
49 inline procedural "cic:/Coq/Init/Datatypes/bool.ind".
55 (*#* [nat] is the datatype of natural numbers built from [O] and successor [S];
56 note that zero is the letter O, not the numeral 0 *)
58 inline procedural "cic:/Coq/Init/Datatypes/nat.ind".
61 Delimit Scope nat_scope with nat.
65 Bind Scope nat_scope with nat.
69 Arguments Scope S [nat_scope].
72 (*#* [Empty_set] has no inhabitant *)
74 inline procedural "cic:/Coq/Init/Datatypes/Empty_set.ind".
76 (*#* [identity A a] is the family of datatypes on [A] whose sole non-empty
77 member is the singleton datatype [identity A a a] whose
78 sole inhabitant is denoted [refl_identity A a] *)
80 inline procedural "cic:/Coq/Init/Datatypes/identity.ind".
83 Hint Resolve refl_identity: core v62.
87 Implicit Arguments identity_ind [A].
91 Implicit Arguments identity_rec [A].
95 Implicit Arguments identity_rect [A].
98 (*#* [option A] is the extension of A with a dummy element None *)
100 inline procedural "cic:/Coq/Init/Datatypes/option.ind".
103 Implicit Arguments None [A].
106 (*#* [sum A B], equivalently [A + B], is the disjoint sum of [A] and [B] *)
108 (* Syntax defined in Specif.v *)
110 inline procedural "cic:/Coq/Init/Datatypes/sum.ind".
113 Notation "x + y" := (sum x y) : type_scope.
116 (*#* [prod A B], written [A * B], is the product of [A] and [B];
117 the pair [pair A B a b] of [a] and [b] is abbreviated [(a,b)] *)
119 inline procedural "cic:/Coq/Init/Datatypes/prod.ind".
122 Add Printing Let prod.
126 Notation "x * y" := (prod x y) : type_scope.
130 Notation "( x , y , .. , z )" := (pair .. (pair x y) .. z) : core_scope.
138 cic:/Coq/Init/Datatypes/projections/A.var
142 cic:/Coq/Init/Datatypes/projections/B.var
145 inline procedural "cic:/Coq/Init/Datatypes/fst.con" as definition.
147 inline procedural "cic:/Coq/Init/Datatypes/snd.con" as definition.
154 Hint Resolve pair inl inr: core v62.
157 inline procedural "cic:/Coq/Init/Datatypes/surjective_pairing.con" as lemma.
159 inline procedural "cic:/Coq/Init/Datatypes/injective_projections.con" as lemma.
163 inline procedural "cic:/Coq/Init/Datatypes/comparison.ind".
165 inline procedural "cic:/Coq/Init/Datatypes/CompOpp.con" as definition.