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
29
|
\DOC occurs_in
\TYPE {occurs_in : hol_type -> hol_type -> bool}
\SYNOPSIS
Tests if one type occurs in another.
\DESCRIBE
The call {occurs_in ty1 ty2} returns {true} if {ty1} occurs as a subtype of
{ty2}, including the case where {ty1} and {ty2} are the same. If returns
{false} otherwise. The type {ty1} does not have to be a type variable.
\FAILURE
Never fails.
\EXAMPLE
{
# occurs_in `:A` `:(A)list->bool`;;
val it : bool = true
# occurs_in `:num->num` `:num->num->bool`;;
val it : bool = false
# occurs_in `:num->bool` `:num->num->bool`;;
val it : bool = true
}
\SEEALSO
free_in, tyvars, vfree_in.
\ENDDOC
|
