### FREE-VARIABLES-TYPE-PRESCRIPTION

matching for free variable in type-prescription rules
```Major Section:  FREE-VARIABLES
```

We assume familiarity with the issue of dealing with free variables in hypotheses; see free-variables.

By default, starting with Version 4.3, ACL2 attempts all possible matches for free variables. Consider the following example.

```(defstub f1 (x) t)
(defstub f2 (x y) t)
(defstub f3 (y) t)

(defaxiom f1-prop
(implies (and (f2 x y) ; <-- y is free in this hypothesis
(f3 y))
(f1 x))       ; <-- (f1 x) is the type-term (type is `non-nil')
:rule-classes :type-prescription)

; Succeeds:
(thm (implies (and (f2 a b)
(f3 b))
(f1 a)))

; The following fails unless we try more than one match for free variables in
; hypotheses.
(thm (implies (and (f2 a b)
(f2 a c)
(f2 a d)
(f3 b))
(f1 a)))
```

There may be times when you want to match only the first free variable. In that case, you can write a function of two arguments, the type-prescription rune being applied and the current ACL2 world, that prohibits multiple matching for those times. Your function is then `attached' to the built-in constrained function, `oncep-ts`. The following examples are intended to explain how this works.

First, let us disallow all mutliple matching of free variables (i.e., implement the behavior often referred to as ```:match-free :once`''; see free-variables).

```(defun oncep-tp-always (rune wrld)
(declare (ignore rune wrld)
(xargs :mode :logic :guard t))
t)

(defattach oncep-tp oncep-tp-always)
```
The second `thm` form above will now fail, because only one free-variable match is permitted for the first hypothesis of rule `f1-prop` above.

Now suppose that instead, we want to disallow multiple matches for free variables in hypotheses of type-prescription rules except for the rule `f1-prop` above. With the following events, the second `thm` form above once again succeeds.

```(defun oncep-tp-always-except-f1-prop (rune wrld)
(declare (ignore wrld)
(xargs :mode :logic :guard (and (consp rune)
(consp (cdr rune))
(symbolp (cadr rune)))))
(not (eq (base-symbol rune) 'f1-prop)))

(defattach oncep-tp oncep-tp-always-except-f1-prop)
```

In general, your `defattach` event will attach a function symbol to `oncep-tp`. The guard of that function symbol must be implied by the tuard of `oncep-tp`:

```ACL2 !>:args oncep-tp

Function         ONCEP-TP
Formals:         (RUNE WRLD)
Signature:       (ONCEP-TP * *)
=> *
Guard:           (AND (PLIST-WORLDP WRLD)
(CONSP RUNE)
(CONSP (CDR RUNE))
(SYMBOLP (CADR RUNE)))
Guards Verified: T
Defun-Mode:      :logic
Type:            built-in (or unrestricted)

ONCEP-TP
ACL2 !>
```