/usr/share/hol88-2.02.19940316/help/ENTRIES/aconv.doc is in hol88-help 2.02.19940316-35.
This file is owned by root:root, with mode 0o644.
The actual contents of the file can be viewed below.
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 26 27 28 | \DOC aconv
\TYPE {aconv : (term -> term -> bool)}
\SYNOPSIS
Tests for alpha-convertibility of terms.
\KEYWORDS
alpha.
\DESCRIBE
When applied to two terms, {aconv} returns {true} if they are
alpha-convertible, and {false} otherwise.
\FAILURE
Never fails.
\EXAMPLE
A simple case of alpha-convertibility is the renaming of a single quantified
variable:
{
#aconv "?x. x=T" "?y. y=T";;
true : bool
}
\SEEALSO
ALPHA, ALPHA_CONV.
\ENDDOC
|