TAU-INTERVAL-DOM

access the domain of a tau interval
Major Section:  TAU-SYSTEM

It is the case that

(tau-interval-dom (make-tau-interval dom lo-rel lo hi-rel hi)) = dom

For a well-formed interval, dom is one of the symbols INTEGERP, RATIONALP, ACL2-NUMBERP, or NIL. When the domain is NIL there is no domain restriction.

When the domain is INTEGERP, there are additional constraints on the other components. See make-tau-interval.