core_1 Theory
Defines display forms for primitive terms of Nuprl's type
theory, and introduces abstractions for propositions-as-types
correspondence. Also contains precedence objects that control
parenthesization of displays.
Summary of Definitions
Typed Definitions
-
member *
-
-
unit *
-
-
true *
-
-
false *
-
-
and *
-
-
or *
-
-
implies *
-
-
rev_implies *
-
-
squash *
-
-
not *
-
-
nequal *
-
-
iff *
-
-
exists *
-
-
sq_exists *
-
-
all *
-
-
le *
-
-
ge *
-
-
gt *
-
Main Theorems
Listing
Last modified February 24th, 1995
Paul Jackson /
jackson@cs.cornell.edu