## TYPE-PRESCRIPTION

make a rule that specifies the type of a term
```Major Section:  RULE-CLASSES
```

See rule-classes for a general discussion of rule classes and how they are used to build rules from formulas. Some example `:``corollary` formulas from which `:type-prescription` rules might be built are:

```Examples:
(implies                           (nth n lst) is of type characterp
(and (character-listp lst)        provided the two hypotheses can
(< n (length lst)))          be established by type reasoning
(characterp (nth n lst))).

(implies                           (demodulize a lst 'value ans) is
(and (atom a)                     either a nonnegative integer or
(true-listp lst)             of the same type as ans, provided
(member-equal a lst))        the hyps can be established by type
(or (and                          reasoning
(integerp
(demodulize a lst 'value ans))
(>= (demodulize a lst 'value ans) 0))
(equal (demodulize a lst 'value ans) ans))).
```
To specify the term whose type (see type-set) is described by the rule, provide that term as the value of the `:typed-term` field of the rule class object.

```General Form:
(implies hyps
(or type-restriction1-on-pat
...
type-restrictionk-on-pat
(equal pat var1)
...
(equal pat varj)))
```
where `pat` is the application of some function symbol to some arguments, each `type-restrictioni-on-pat` is a term involving `pat` and containing no variables outside of the occurrences of `pat`, and each `vari` is one of the variables of `pat`. Generally speaking, the `type-restriction` terms ought to be terms that inform us as to the type of `pat`. Ideally, they should be ``primitive recognizing expressions'' about `pat`; see compound-recognizer.

If the `:typed-term` is not provided in the rule class object, it is computed heuristically by looking for a term in the conclusion whose type is being restricted. An error is caused if no such term is found.

Roughly speaking, the effect of adding such a rule is to inform the ACL2 typing mechanism that `pat` has the type described by the conclusion, when the hypotheses are true. In particular, the type of `pat` is within the union of the types described by the several disjuncts. The ``type described by'' `(equal pat vari)` is the type of `vari`.

More operationally, when asked to determine the type of a term that is an instance of `pat`, ACL2 will first attempt to establish the hypotheses. This is done by type reasoning alone, not rewriting! Of course, if some hypothesis is to be forced, it is so treated; see force and see case-split. So-called free variables in hypotheses are treated specially; see free-variables. Provided the hypotheses are established by type reasoning, ACL2 then unions the types described by the `type-restrictioni-on-pat` terms together with the types of those subexpressions of `pat` identified by the `vari`. The final type computed for a term is the intersection of the types implied by each applicable rule. Type prescription rules may be disabled.

Because only type reasoning is used to establish the hypotheses of `:type-prescription` rules, some care must be taken with the hypotheses. Suppose, for example, that the non-recursive function `my-statep` is defined as

```  (defun my-statep (x)
(and (true-listp x)
(equal (length x) 2)))
```
and suppose `(my-statep s)` occurs as a hypothesis of a `:type-prescription` rule that is being considered for use in the proof attempt for a conjecture with the hypothesis `(my-statep s)`. Since the hypothesis in the conjecture is rewritten, it will become the conjunction of `(true-listp s)` and `(equal (length s) 2)`. Those two terms will be assumed to have type `t` in the context in which the `:type-prescription` rule is tried. But type reasoning will be unable to deduce that `(my-statep s)` has type `t` in this context. Thus, either `my-statep` should be disabled (see disable) during the proof attempt or else the occurrence of `(my-statep s)` in the `:type-prescription` rule should be replaced by the conjunction into which it rewrites.

While this example makes it clear how non-recursive predicates can cause problems, non-recursive functions in general can cause problems. For example, if `(mitigate x)` is defined to be `(if (rationalp x) (1- x) x)` then the hypothesis `(pred (mitigate s))` in the conjecture will rewrite, opening `mitigate` and splitting the conjecture into two subgoals, one in which `(rationalp s)` and `(pred (1- x))` are assumed and the other in which `(not (rationalp s))` and `(pred x)` are assumed. But `(pred (mitigate s))` will not be typed as `t` in either of these contexts. The moral is: beware of non-recursive functions occuring in the hypotheses of `:type-prescription` rules.

Because of the freedom one has in forming the conclusion of a type-prescription, we have to use heuristics to recover the pattern, `pat`, whose type is being specified. In some cases our heuristics may not identify the intended term and the `:type-prescription` rule will be rejected as illegal because the conclusion is not of the correct form. When this happens you may wish to specify the `pat` directly. This may be done by using a suitable rule class token. In particular, when the token `:type-prescription` is used it means ACL2 is to compute pat with its heuristics; otherwise the token should be of the form `(:type-prescription :typed-term pat)`, where `pat` is the term whose type is being specified.

The defun event may generate a `:type-prescription` rule. Suppose `fn` is the name of the function concerned. Then `(:type-prescription fn)` is the rune given to the type-prescription, if any, generated for `fn` by `defun`. (The trivial rule, saying `fn` has unknown type, is not stored, but `defun` still allocates the rune and the corollary of this rune is known to be `t`.)