-
Notifications
You must be signed in to change notification settings - Fork 0
wf of terms
The first step in creating the logic is to declare a term to define well-formedness of expressions. We use the term type to provide a well-formedness type judgment. Proofs of well-formedness are computationally meaningless, and we also declare a trivial proof term trivial.
To form this judgment we create a module Fol_type. First, create an interface:
Create the file fol_type.mli
, containing the line:
declare "type"{'A}
declare trivial
The intent of this term is that if the expression type{'t}
is provable, then the term 't
is a well-formed formula.
Next, we create the implementation. The rules for well-formedness will be stated in the module for the logical operators, so the only implementation we need to include is the syntax declaration and a display form to produce pretty output.
Create the file fol_type.ml
containing the following lines:
include Base_theory
declare "type"{'A}
declare trivial
dform type_df : "type"{'A} = slot{'A} `" type"
dform trivial_df : trivial = cdot
The Base_theory
is included for basic logic and display form definitions. The display form prints the term type{'t}
as the term 't
type. The trivial
term is printed as the single character \cdot
, which is defined in the Nuprl_font
module in the Base_theory
theory.
Next we are going to compile this theory.
Edit MetaprlInfo
file:
THEORYNAME = fol
THEORYDESCR = First-Order Logic
THEORY_DEPS[] +=
itt/core
# Library files
MPFILES[] =
fol_type
then execute % omake
in shell.
Now the module is compiled and linked with the editor, and we can view this theory in the editor.