File: it.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 (28 lines) | stat: -rw-r--r-- 492 bytes parent folder | download | duplicates (7)
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
\DOC it

\TYPE {it : 'a}

\SYNOPSIS
Binds the value of the last expression evaluated at top level.

\DESCRIBE
The identifier {it} is bound to the value of the last expression evaluated
at top level. Declarations do not effect the value of {it}.

\EXAMPLE
{
  # 2 + 3;;
  val it : int = 5
  # let x = 2*3;;
  val x : int = 6
  # it;;
  val it : int = 5
  # it + 12;;
  val it : int = 17
}

\USES
Used in evaluating expressions that require the value of the last evaluated
expression.

\ENDDOC