File: set_lambda.doc

package info (click to toggle)
hol88 2.02.19940316dfsg-5
  • links: PTS
  • area: main
  • in suites: bookworm
  • size: 65,816 kB
  • sloc: ml: 199,939; ansic: 9,666; sh: 6,913; makefile: 6,032; lisp: 2,747; yacc: 894; sed: 201; cpp: 87; awk: 5
file content (31 lines) | stat: -rw-r--r-- 724 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
27
28
29
30
31
\DOC set_lambda

\TYPE {set_lambda : (string -> string)}

\SYNOPSIS
Sets the `lambda' symbol used in printing terms.

\DESCRIBE
If {s} is a string, then {set_lambda s} sets to {s} the `lambda' symbol (by
default `{\}') which is used to represent lambda-abstraction in terms.
The call returns the previous string used for this purpose. The call affects
the printing of terms, but the original symbol is still expected by the
quotation parser.

\FAILURE
Never fails.

\EXAMPLE
In the following, the lambda symbol is set to `{fn}', and the effect on the
printing of a typical term is illustrated.
{
   #set_lambda `fn`;;
   `\` : string

   #"\x. SUC x";;
   "fn x. SUC x" : term
}
\SEEALSO
set_prompt, set_turnstile.

\ENDDOC