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
30
31
32
33
|
\DOC new_binder
\TYPE {new_binder : ((string # type) -> void)}
\SYNOPSIS
Sets up a new binder in the current theory.
\DESCRIBE
A call {new_binder(`bnd`,":ty")} declares a new binder {bnd} in the current
theory. The type must be of the form {(* -> **) -> ***}, because being a binder,
{bnd} will apply to an abstraction; for example {"!x:bool. (x=T) \/ (x=F)"} is
actually a prettyprinting of {"$! (\x. (x=T) \/ (x=F))"}.
\FAILURE
Fails if HOL is not in draft mode, or there is already a constant of some sort
of that name in the current theory, or if the type does not correspond to the
above pattern.
\EXAMPLE
{
#new_theory `anorak`;;
() : void
#new_binder(`!!`,":(bool->bool)->bool");;
() : void
#"!!x. T";;
"!! x. T" : term
}
\SEEALSO
binders, is_binder.
\ENDDOC
|
