File: mk_let.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 (29 lines) | stat: -rw-r--r-- 546 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
 
\DOC mk_let

\TYPE {mk_let : ((term # term) -> term)}

\SYNOPSIS
Constructs a {let} term.

\DESCRIBE
{mk_let("f","x")} returns {"LET f x"}. If {f} is of the form {"\y. t"} then
the result will be pretty-printed as {"let y=x in t"}.

\FAILURE
Fails with {mk_let} if the types of {f} and {x} are such that {"LET f x"} is
not well-typed. {"LET"} has most general type:
{
   ":(* -> **) -> * -> **"
}
\EXAMPLE
{
#mk_let("$= 1","2");;
"LET($= 1)2" : term

#mk_let("\x. x = 1","2");;
"let x = 2 in (x = 1)" : term
}
\SEEALSO
dest_let, is_let.

\ENDDOC