File: let_before.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 (46 lines) | stat: -rw-r--r-- 967 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
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
\DOC let_before

\TYPE {let_before : ((string # string # string list) -> void)}

\SYNOPSIS
Makes an ML declaration dynamically before other pending declarations.

\DESCRIBE
The call
{
   let_before(`x`,`f`,[`arg1`;...;`argn`])
}
\noindent puts an ML declaration
{
   let x = f [`arg1`;...;`argn`];;
}
\noindent at the head of the queue of currently pending toplevel items. It will
be evaluated after the phrase which invoked {let_before}. This gives a way of
performing declarations dynamically. Note that the first two argument strings
are interpreted as single identifiers, whereas the arguments are passed as
literal strings.

\FAILURE
Never fails, although the subsequent declaration may well fail for any of the
usual reasons.

\EXAMPLE
{
#let fn = \l:(string)list. 1;;
fn = - : (string list -> int)

#let_before(`x`,`fn`,[]);;
() : void

x = 1 : int

#x;;
1 : int
}
\USES
Performing variants on autoloading.

\SEEALSO
inject_input, let_after, ML_eval.

\ENDDOC