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___,, * INRIA-Rocquencourt & LRI-CNRS-Orsay *)
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: Params.v,v 1.2 2002/02/14 14:39:04 filliatr Exp $ i*)
36 Axiomatisation of a numerical set
38 It will be instantiated by Z and R later on
39 We choose to introduce many operation to allow flexibility in definition
40 ([S] is primitive in the definition of [nat] while [add] and [one]
41 are primitive in the definition
44 inline procedural "cic:/Coq/Num/Params/N.con".
46 inline procedural "cic:/Coq/Num/Params/zero.con".
48 inline procedural "cic:/Coq/Num/Params/one.con".
50 inline procedural "cic:/Coq/Num/Params/add.con".
52 inline procedural "cic:/Coq/Num/Params/S.con".
54 (*#* Relations, equality is defined separately *)
56 inline procedural "cic:/Coq/Num/Params/lt.con".
58 inline procedural "cic:/Coq/Num/Params/le.con".
60 inline procedural "cic:/Coq/Num/Params/gt.con".
62 inline procedural "cic:/Coq/Num/Params/ge.con".