`numbervars/3`

[meta_logic]`numbervars(`

`+Term``, `

`+FirstVar``, `

`-LastVar``)`

instantiates each of the variables in `Term` to a term of the form
`'$VAR'(`

`N``)`

.

`Term`- term
`FirstVar`- integer, must be nonvar
`LastVar`- integer

`FirstVar` is used as the value of `N` for the first variable
in `Term` (starting from the left). The second distinct variable
in `Term` is given a value of `N` satisfying “`N` is
`FirstVar`+1”; the third distinct variable gets the value
`FirstVar`+2, and so on. The last variable in `Term` has the
value `LastVar`-1.

Notice that in the example below, `display/1`

is used rather than
`write/1`

. This is because `write/1`

treats terms of the
form `'$VAR'(`

`N``)`

specially; it writes ``A`' if
`N`=0, ``B`' if `N`=1, ...``Z`' if `N`=25,
``A1`' if `N`=26, etc. That is why, if you type the goal in
the example below, the variable bindings will also be printed out as
follows:

Term = foo(W,W,X), A = W, B = X

`instantiation_error`

`FirstVar`is uninstantiated`type_error`

`FirstVar`is not an integer

| ?-Term = foo(A, A, B), numbervars(Term, 22, _), display(Term).foo($VAR(22),$VAR(22),$VAR(23))

ref-lte-anv, `listing/[0,1]`

, `write_term/[2,3]`

.

Send feedback on this subject.