Sorts

Individual sorts are defined as well as the following sorts and sort operations:

abstraction
bindings
cell
data
datum
distinct-datum
integer
list
list-of(_)
map
map-of(_,_)
natural
number
real
set
set-of(_)
storage
token
transients
truth-value
tuple

join(_,_) :: (sort,sort) -> sort
meet(_,_) :: (sort,sort) -> sort
subsort(_,_) :: (sort,sort) -> truth-value

Is

_ is _

Tuples

count _ :: tuple -> natural
first _ :: tuple -> datum
nth-component-of :: natural,tuple -> datum
rest _ :: tuple -> tuple
tuple _ :: (datum,datum) -> tuple

Truth-Values

both _ :: (truth-value,truth-value) -> truth-value
either _ :: (truth-value,truth-value) -> truth-value
if _ then _ else _ :: truth-value,x,y -> x | y
not _ :: truth-value -> truth-value

Numbers (Naturals, Integers, Reals)

difference(_,_)
is-greater-than(_,_)
is-less-than(_,_)
natural(_)
negation(_)
predecessor(_)
product(_,_)
quotient(_,_)
successor(_)
sum(_,_)

Lists

components-of(_)
concatenation(_,_)
empty-list
head-of(_)
length-of(_)
list(_)
reverse(_)
tail-of(_)

Sets

difference-set(_,_)
disjoint-union(_,_)
empty-set
intersection(_,_)
is-in(_,_)
is-subset-of(_,_)
set(_)
size-of(_)
union(_,_)

Maps

at(_,_)
domain-of(_)
empty-map
map-to(_,_)
merge(_,_)
omission(_,_)
overlay(_,_)
range-of(_)