File: frees.doc

package info (click to toggle)
hol88 2.02.19940316dfsg-5
  • links: PTS
  • area: main
  • in suites: bookworm
  • size: 65,816 kB
  • sloc: ml: 199,939; ansic: 9,666; sh: 6,913; makefile: 6,032; lisp: 2,747; yacc: 894; sed: 201; cpp: 87; awk: 5
file content (25 lines) | stat: -rw-r--r-- 547 bytes parent folder | download | duplicates (11) 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
 
\DOC frees

\TYPE {frees : (term -> term list)}

\SYNOPSIS
Returns a list of the variables which are free in a term.

\DESCRIBE
When applied to a term, {frees} returns a list of the free variables in
that term. There are no repetitions in the list produced even if there are
multiple free instances of some variables.

\FAILURE
Never fails.

\EXAMPLE
Clearly in the following term, {x} and {y} are free, whereas {z} is bound:
{
   #frees "(x=1) /\ (y=2) /\ (!z. z >= 0)";;
   ["x"; "y"] : term list
}
\SEEALSO
freesl, free_in, thm_frees.

\ENDDOC