File: it.doc

package info (click to toggle)
hol-light 20170109-1
  • links: PTS, VCS
  • area: main
  • in suites: stretch
  • size: 36,568 kB
  • ctags: 8,549
  • sloc: ml: 540,018; cpp: 439; lisp: 286; java: 279; makefile: 262; sh: 229; yacc: 108; perl: 78; ansic: 57; sed: 39
file content (28 lines) | stat: -rw-r--r-- 492 bytes parent folder | download | duplicates (6)
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