File: temp_path.doc

package info (click to toggle)
hol-light 20190729-4
  • links: PTS, VCS
  • area: main
  • in suites: bullseye
  • size: 42,676 kB
  • sloc: ml: 637,078; cpp: 439; makefile: 301; lisp: 286; java: 279; sh: 239; yacc: 108; perl: 78; ansic: 57; sed: 39; python: 13
file content (25 lines) | stat: -rw-r--r-- 389 bytes parent folder | download | duplicates (4) 
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
 
\DOC temp_path

\TYPE {temp_path : string ref}

\SYNOPSIS
Directory in which to create temporary files.

\DESCRIBE
Some HOL Light derived rules in the libraries (none in the core system) need to 
create temporary files. This is the directory in which they do so.

\FAILURE
Not applicable.

\EXAMPLE
On my laptop:
{
  # !temp_path;;
  val it : string = "/tmp"
}

\SEEALSO
hol_dir.

\ENDDOC