diff options
Diffstat (limited to 'theories/Num/Definitions.v')
-rw-r--r-- | theories/Num/Definitions.v | 20 |
1 files changed, 20 insertions, 0 deletions
diff --git a/theories/Num/Definitions.v b/theories/Num/Definitions.v new file mode 100644 index 000000000..defb12897 --- /dev/null +++ b/theories/Num/Definitions.v @@ -0,0 +1,20 @@ +(*i $Id $ i*) + +(*s + Axiomatisation of a numerical set + It will be instantiated by Z and R later on + We choose to introduce many operation to allow flexibility in definition + ([S] is primitive in the definition of [nat] while [add] and [one] + are primitive in the definition +*) + +Parameter N:Type. +Parameter zero:N. +Parameter one:N. +Parameter add:N->N->N. +Parameter S:N->N. + +(*s Relations *) +Parameter eq,lt,le,gt,ge:N->N->Prop. +Definition neq [x,y:N] := (eq x y)->False. + |