Nuprl Terms

Table 5: Terms in Nuprl's computation language Term Name Prec Assoc Description [var] var variable [var].[term] lam 6 lambda [term] [term] ap 10 L apply <[term],[term]> pair pair [pair term].1 pi1 11 lhs of pair [pair term].2 pi2 11 rhs of pair [natural] natnum natural number -[int] minus 10 unary minus [int] * [int] mul 9 L multiply [int] + [int] add 8 L add [int] - [int] sub 8 subtract

**Table 5:** Terms in Nuprl's computation language
Term	Name	Prec	Assoc	Description
[var]	var			variable
$\lambda$ [var].[term]	lam	6		lambda
[term] [term]	ap	10	L	apply
<[term],[term]>	pair			pair
[pair term].1	pi1	11		lhs of pair
[pair term].2	pi2	11		rhs of pair
[natural]	natnum			natural number
-[int]	minus	10		unary minus
[int] * [int]	mul	9	L	multiply
[int] + [int]	add	8	L	add
[int] - [int]	sub	8		subtract

Table 6: Types Term Name Prec Assoc Description {[level]} prop propositional universe {[level]} univ type universe [prop] [prop] prod 6 R product type [prop] [prop] fun 6 R function type int integer type

**Table 6:** Types
Term	Name	Prec	Assoc	Description
${\Bbb{P}}$ `{`[level]`}`	prop			propositional universe
$\Bbb{U}$ `{`[level]`}`	univ			type universe
[prop] $\times$ [prop]	prod	6	R	product type
[prop] $\rightarrow$ [prop]	fun	6	R	function type
$\Bbb{Z}$	int			integer type

Table 7: Propositions Term Name Prec Assoc Description True true true False false false [int] [int] le 5 R less than or equal [int] [int] lt 5 R less than [term] = [term] [type] equal 5 R equality [int] = [int] eqi 5 R equality over Z (abbr. of equal) [prop] not 6 not [prop] [prop] and 4 L and [prop] [prop] or 4 L or [prop] [prop] implies 3 R implies [prop] [prop] rev_implies 3 L is implied by [prop] [prop] iff 2 if and only if [var]:[type]. [prop] all 1 universal quantifier [var]:[type]. [prop] exists 1 existential quantifier

**Table 7:** Propositions
Term	Name	Prec	Assoc	Description
True	true			true
False	false			false
[int] $\leq$ [int]	le	5	R	less than or equal
[int] [int]	lt	5	R	less than
[term] = [term] $\in$ [type]	equal	5	R	equality
[int] = [int]	eqi	5	R	equality over Z
				(abbr. of `equal`)
$\neg$ [prop]	not	6		not
[prop] $\wedge$ [prop]	and	4	L	and
[prop] $\vee$ [prop]	or	4	L	or
[prop] $\Rightarrow$ [prop]	implies	3	R	implies
[prop] $\Leftarrow$ [prop]	rev_implies	3	L	is implied by
[prop] $\Longleftrightarrow$ [prop]	iff	2		if and only if
$\forall$ [var]:[type]. [prop]	all	1		universal quantifier
$\exists$ [var]:[type]. [prop]	exists	1		existential quantifier

Table 5 lists terms in the computational fragment of Nuprl's object language. Table 6 lists the terms for types and Table 7 lists the terms for propositional and predicate logic.

The `Prec' column in the tables is for the precedence of the term. The `Assoc' column gives the associativity of infix terms. This information simplifies slightly how the pretty-printer calculates when to add parentheses. In practice, slightly more parentheses might be inserted than you might expect from the information in the tables.