diff options
Diffstat (limited to 'theories/Numbers/NatInt')
| -rw-r--r-- | theories/Numbers/NatInt/NZAxioms.v | 6 |
1 files changed, 6 insertions, 0 deletions
diff --git a/theories/Numbers/NatInt/NZAxioms.v b/theories/Numbers/NatInt/NZAxioms.v index 4dedcfe32b..fcd98787f9 100644 --- a/theories/Numbers/NatInt/NZAxioms.v +++ b/theories/Numbers/NatInt/NZAxioms.v @@ -137,3 +137,9 @@ Module Type NZDecOrdSig' := NZOrdSig' <+ HasCompare. Module Type NZDecOrdAxiomsSig := NZOrdAxiomsSig <+ HasCompare. Module Type NZDecOrdAxiomsSig' := NZOrdAxiomsSig' <+ HasCompare. +(** A square function *) + +Module Type NZSquare (Import NZ : NZBasicFunsSig'). + Parameter Inline square : t -> t. + Axiom square_spec : forall n, square n == n * n. +End NZSquare. |