Major Section: TAU-SYSTEM
General Form: (make-tau-interval doc lo-rel lo hi-rel hi)
An interval is a structure of the form:
)). Every tau contains an
interval used to represent the domain, the upper, and the lower bounds of the
objects recognized by the tau.
make-tau-interval constructs well-formed intervals only if its five arguments
satisfy certain restrictions given below. When these restrictions are
make-tau-interval can construct objects that are not intervals!
make-tau-interval does not attempt to coerce or adjust its arguments to make
For examples of intervals (and non-intervals!) constructed by
tau-intervalp. For examples of what objects are
contained in certain intervals, see
The components of an interval are as follows:
dom (``domain'') -- must be one of four symbols:
NIL denoting no restriction
on the domain.
The two ``relations,'' lo-rel and hi-rel are Booleans, where
denotes less-than inequality (
less-than-or-equal inequality (
<=). Think of
t meaning ``strong''
nil meaning ``weak'' inequality.
Lo and hi must be either
nil or explicit rational numbers. If
nil it denotes negative infinity; if hi is
denotes positive infinity. Lo must be no greater than hi.
Note: Even though
ACL2-NUMBERP intervals may contain complex
rationals, the lo and hi bounds must be rational. This is an
arbitrary decision made by the implementors to simplify coding.
Finally, if the dom is
INTEGERP, then both relations should be weak
and lo and hi must be integers when they are non-
For x to be ``in'' an interval it must be of the type described by the domain predicate dom, lo must be smaller than x in the strong or weak sense denoted by lo-rel, and x must be smaller than hi in the strong or weak sense denoted by hi-rel.
The components of an interval may be accessed with the functions