Documentation out of dateLearn more
%use
A %use directive adds a constraint domain to the current STELF signature.
Like some other directives, for instance %clause, it is incompatible with STELF’s ability to verify totality assertions and metatheorems.
See also
Section titled “See also”- Constraint domains
- Constraint domains (guide §6.32)