aboutsummaryrefslogtreecommitdiff
path: root/src/algebra/complet.spad.pamphlet
diff options
context:
space:
mode:
Diffstat (limited to 'src/algebra/complet.spad.pamphlet')
-rw-r--r--src/algebra/complet.spad.pamphlet4
1 files changed, 2 insertions, 2 deletions
diff --git a/src/algebra/complet.spad.pamphlet b/src/algebra/complet.spad.pamphlet
index 5ac5d928..d6d6244d 100644
--- a/src/algebra/complet.spad.pamphlet
+++ b/src/algebra/complet.spad.pamphlet
@@ -79,7 +79,7 @@ OrderedCompletion(R:SetCategory): Exports == Implementation where
n:Integer * x:% ==
x case inf =>
- n > 0 => x
+ positive? n => x
negative? n => [not(x.inf)]
error "Undefined product"
[n * x.fin]
@@ -103,7 +103,7 @@ OrderedCompletion(R:SetCategory): Exports == Implementation where
characteristic == characteristic$R
fininf(b, r) ==
- r > 0 => [b]
+ positive? r => [b]
negative? r => [not b]
error "Undefined product"