MetaPRL Base Syntax

The MetaPRL compiler defines syntax in two modules: the Perv module, defined in the directory theories/tactic/perv.mli, and the Summary module, defined in theories/base/summary.mli. These modules have two different purposes: the Perv module defines terms that are commonly use to represent refiner primitives: it includes a list construction with cons and nil terms, a primitive lambda abstraction, and a sequent representation.

The Summary module provides the syntax for theories. It contains one or more term declarations for each of the syntax constructions in a MetaPRL theory module. These constructions may contain OCaml programs; the programs are defined in the file theories/ocaml/ocaml.mli.

The Nuprl_font module defines the character set used in MetaPRL for displaying terms. The character set defined for MetaPRL 2.00.1 is the following:

mathbbA :
mathbbB :
mathbbC :
mathbbD :
mathbbE :
mathbbF :
mathbbG :
mathbbH :
mathbbI :
mathbbJ :
mathbbK :
mathbbM :
mathbbN :
mathbbO :
mathbbP :
mathbbQ :
mathbbR :
mathbbS :
mathbbT :
mathbbU :
mathbbV :
mathbbW :
mathbbX :
mathbbY :
shortLeftarrow : 5
leftarrow :
middlearrow :
shortRightarrow :
rightarrow :
leftrightarrow :
ulcorner :
urcorner :
vdash
integral :
cdot
downarrow :
uparrow :
alpha
beta :
pi :
lambda :
gamma :
delta :
rho :
sigma :
epsilon :
eta :
theta :
iota :
kappa :
mu :
nu :
omicron :
tau :
phi :
xi :
omega :
wedge :
tneg :
member :
plusminus :
oplus : XXX
infty : XXX
partial :
subset :
supset :
cap :
cup :
forall :
exists :
oinfty : XXX
shortleftrightarrow :
shortleftarrow :
shortrightarrow :
longleftrightarrow :
longleftarrow :
longrightarrow :
neq : 225
sim : XXX
le :
ge :
equiv :
vee :
leftarrow :
middlearrow :
rightarrow :
sigma :
delta :
pi :
times :
div
supplus :
supminus :
supcirc :
subseteq :
supseteq :
subzero :
subone :
subtwo :
subthree :
suba :
subb :
subc :
subq : XXX
subz :