diff options
Diffstat (limited to 'theories/Num/Leibniz/Params.v')
| -rw-r--r-- | theories/Num/Leibniz/Params.v | 20 |
1 files changed, 0 insertions, 20 deletions
diff --git a/theories/Num/Leibniz/Params.v b/theories/Num/Leibniz/Params.v deleted file mode 100644 index c8cb772de..000000000 --- a/theories/Num/Leibniz/Params.v +++ /dev/null @@ -1,20 +0,0 @@ -(*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, equality is defined separately *) -Parameter lt,le,gt,ge:N->N->Prop. - - |