diff options
Diffstat (limited to 'src/algebra/catdef.spad.pamphlet')
| -rw-r--r-- | src/algebra/catdef.spad.pamphlet | 42 |
1 files changed, 41 insertions, 1 deletions
diff --git a/src/algebra/catdef.spad.pamphlet b/src/algebra/catdef.spad.pamphlet index 4b0eb27e..b67de306 100644 --- a/src/algebra/catdef.spad.pamphlet +++ b/src/algebra/catdef.spad.pamphlet @@ -227,6 +227,45 @@ BasicType(): Category == Type with @ +\section{Ordered Types} + +<<category ORDTYPE OrderedType>>= +)abbrev category ORDTYPE OrderedType +++ Author: Gabriel Dos Reis +++ Date Created: June 28, 2010 +++ Date Last Modified: June 28, 2010 +++ See Also: OrderedSet +++ Description: +++ Category of types equipped with a total ordering. +++ Axioms: +++ forall(x,y) +++ x > y = y < x +++ x <= y = not(y > x) +++ x >= y = not(x < y) +OrderedType(): Category == BasicType with + < : (%,%) -> Boolean + ++ \spad{x < y} holds if \spad{x} is less than \spad{y} in the + ++ current domain. + > : (%,%) -> Boolean + ++ \spad{x > y} holds if \spad{x} is greater than \spad{y} in the + ++ current domain. + <= : (%,%) -> Boolean + ++ \spad{x <= y} holds if \spad{x} is less or equal than \spad{y} + ++ in the current domain. + >= : (%,%) -> Boolean + ++ \spad{x <= y} holds if \spad{x} is greater or equal than \spad{y} + ++ in the current domain. + add + import %before?: (%,%) -> Boolean from Foreign Builtin + x < y == %before?(x,y) + x > y == y < x + x <= y == not(y < x) + x >= y == not(x < y) + x = y == not(x < y) and not(y < x) + +@ + + \section{category BMODULE BiModule} <<category BMODULE BiModule>>= @@ -1971,7 +2010,7 @@ VectorSpace(S:Field): Category == Module(S) with <<license>>= --Copyright (c) 1991-2002, The Numerical ALgorithms Group Ltd. --All rights reserved. ---Copyright (C) 2007-2009, Gabriel Dos Reis. +--Copyright (C) 2007-2010, Gabriel Dos Reis. --All rights reversed. -- --Redistribution and use in source and binary forms, with or without @@ -2006,6 +2045,7 @@ VectorSpace(S:Field): Category == Module(S) with <<license>> <<category BASTYPE BasicType>> +<<category ORDTYPE OrderedType>> <<category SETCAT SetCategory>> <<category STEP StepThrough>> <<category SGROUP SemiGroup>> |