diff options
Diffstat (limited to 'theories/Numbers/Integer/SpecViaZ/ZSig.v')
| -rw-r--r-- | theories/Numbers/Integer/SpecViaZ/ZSig.v | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/theories/Numbers/Integer/SpecViaZ/ZSig.v b/theories/Numbers/Integer/SpecViaZ/ZSig.v index 00e292db0..ef3cd5c34 100644 --- a/theories/Numbers/Integer/SpecViaZ/ZSig.v +++ b/theories/Numbers/Integer/SpecViaZ/ZSig.v @@ -114,4 +114,12 @@ Module Type ZType. Parameter spec_gcd: forall a b, [gcd a b] = Zgcd (to_Z a) (to_Z b). + Parameter sgn : t -> t. + + Parameter spec_sgn : forall x, [sgn x] = Zsgn [x]. + + Parameter abs : t -> t. + + Parameter spec_abs : forall x, [abs x] = Zabs [x]. + End ZType. |