sts
http://www.openmath.org/cd/sts.ocd
2003-04-01
2001-03-12
2
0
official
setname1
Definitions of the symbols used by the OpenMath Small Type System.
type
A symbol to be used within an OpenMath attribute to specify the type of
the object.
The variable z is attributed with a type for complex numbers.
mapsto
This symbol represents the construction of a function type.
The first n-1 children denote the types of the arguments,
the last denotes the return type.
The signature of the power function: (Real , Integer) -> Real
nary
Constructs a child of mapsto which denotes an arbitrary number of
copies of the argument of nary.
The signature for list, an n-ary function:
nassoc
Constructs a child of mapsto which denotes an arbitrary number of
copies of the argument of nassoc. The operator is associative on these
arguments which means that repeated uses may be flattened/unflattened.
The signature for plus, an associative n-ary function:
error
The error symbol is the 'return type' of error symbols in the error
signature file.
structure
The structure element is used to represent a structure of a particular
(algebraic) type.
The signature of a function which given a set will return an element
of that set:
binder
An `OMBIND' object has three parts: a "binder" such as "lambda" or
"for all", a (list of) bound variables, and an expression. The use of
`binder' in a signature indicates that we are describing something
which can only be used as the first child of an OMBIND construct.
The signature of forall is:
attribution
An `attribution' object consists of pairs of keys and values. The use
of the symbol `attribution' in a signature indicates that the symbol
is to be used as a key.
Object
Denotes any OpenMath object.
The signature for list, to show that list has the signature:
Object* -> Object
NumericalValue
Denotes an OpenMath object that is to be thought of as something that
represents a numerical value, or a numerical value.
The generic signature for the function power: