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
34
35
36
37
38
39
40
41
42
43
44
45
|
\DOC parse_as_binder
\TYPE {parse_as_binder : (string -> string)}
\SYNOPSIS
Makes the quotation parser treat a name as a binder.
\DESCRIBE
The call {parse_as_binder `c`} will make the quotation parser treat {c} as a
binder, that is, allow the syntactic sugaring {"c x. y"} as a shorthand for
{"c (\x. y)"}. As with normal binders, e.g. the universal quantifier, the
special syntactic status may be suppressed by preceding {c} with a dollar sign.
\FAILURE
Never fails, even if the string is not an identifier.
\EXAMPLE
{
#new_theory `groof`;;
() : void
#new_definition(`test`,"!! = ($!:(bool->bool)->bool)");;
|- !! = $!
#"!!x.T";;
. cannot be a term
skipping: . T " ;; parse failed
#parse_as_binder `!!`;;
`!!` : string
#"!!x.T";;
"!! x. T" : term
#"$!! (\x. T)";;
"!! x. T" : term
}
\COMMENTS
Special parse status is allotted automatically when a binder is declared, so
this function is unlikely to be needed.
\SEEALSO
activate_all_binders, activate_binders, binders, new_binder.
\ENDDOC
|
