File: type_in.doc

package info (click to toggle)
hol88 2.02.19940316-28
  • links: PTS
  • area: main
  • in suites: jessie, jessie-kfreebsd
  • size: 65,924 kB
  • ctags: 21,595
  • sloc: ml: 199,939; ansic: 9,666; sh: 7,118; makefile: 6,075; lisp: 2,747; yacc: 894; sed: 201; cpp: 87; awk: 5
file content (26 lines) | stat: -rw-r--r-- 482 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
26
 
\DOC type_in

\TYPE {type_in : (type -> term -> bool)}

\SYNOPSIS
Determines whether any subterm of a given term has a particular type.

\DESCRIBE
The predicate {type_in} returns {true} if a subterm of the second argument
has the type specified by the first argument.

\EXAMPLE
{
#type_in ":num" "5 = 4 + 1";;
true : bool

#type_in ":bool" "5 = 4 + 1";;
true : bool

#type_in ":(num)list" "SUC 0";;
false : bool
}
\SEEALSO
find_term, find_terms, type_in_type, type_tyvars.

\ENDDOC