Major Section: TAU-SYSTEM
General Form: (tau-intervalp x)
An interval is a structure of the form:
)). Every tau contains an
interval used to represent the domain and the upper and lower bounds of the
objects recognized by the tau.
Restrictions on the components of an interval are as follows. For an
interpretation of the meaning of the components, see
dom (``domain'') -- must be one of four symbols:
The two ``relations,'' lo-rel and hi-rel, must be Booleans.
Lo and hi must be either
nil or explicit rational numbers.
Lo must be no greater than hi (where
nils represent negative or
positive infinity for lo and hi respectively.
Finally, if the dom is
INTEGERP, then both relations must
and lo and hi must be integers when they are non-
make-tau-interval constructs intervals. The intervals it
constructs are well-formed only if the arguments to
the rules above;
make-tau-interval does not coerce or adjust its
arguments in any way. Thus, it can be (mis-)used to create non-intervals.
Here are examples of
; integers: 0 <= x <= 10: (tau-intervalp (make-tau-interval 'INTEGERP nil 0 nil 10)) = t ; integers: 0 <= x (i.e., the natural numbers): (tau-intervalp (make-tau-interval 'INTEGERP nil 0 nil nil)) = t ; violations of domain rules: (tau-intervalp (make-tau-interval 'INTEGERP t 0 t 10)) = nil (tau-intervalp (make-tau-interval 'INTEGERP nil 0 nil 10/11)) = nil ; violation of rule that bounds must be rational if non-nil: (tau-intervalp (make-tau-interval 'ACL2-NUMBERP t 0 t #c(3 5))) = nil ; violation of rule that lo <= hi: (tau-intervalp (make-tau-interval 'ACL2-NUMBERP t 0 t -10)) = nil ; rationals: 0 < x <= 22/7: (tau-intervalp (make-tau-interval 'RATIONALP t 0 nil 22/7)) = t ; numbers: -10 < x < 10: (tau-intervalp (make-tau-interval 'ACL2-NUMBERP t -10 t 10)) = t ; any: -10 < x < 10: (tau-intervalp (make-tau-interval nil t -10 t 10)) = t : any: (tau-intervalp (make-tau-interval nil nil nil nil nil)) = tNote that the second-to-last interval, with domain
nilcontains all non-numbers as well as numbers strictly between -10 and 10. The reason is that the interval contains
0and all non-numbers are coerced to
0by the inequality functions.
Note that the last interval contains all ACL2 objects. It is called the ``universal interval.''