get start

MetaPRL Tutorial: Getting Started

We will define the logic as in the directory theories/fol. The default OMake configuration only builds itt/core, but you can enable fol by editing the corresponding section in mk/config to:

# This is the list of theory directories theory/* that you want to compile. 
#
# Include itt/core if you want to use the Core of Constructive Type Theory, 
# include itt if you want to use the complete Constructive Type Theory (core,
# applications, extensions, etc).
#
# Alternatively, use THEORIES = all to get all the theories,
# or THEORIES = default, to include the usual set of theories.
# To include your special theory, you would use the following
# if you want the usual directories and your own, use the following.
#    THEORIES = all mytheory
# Or, if you just want your own, use the following.
#    THEORIES = mytheory
#
# If the OMakefile in the theory directory defines the THEORY_DEPS variable,
# the named dependencies will be picked up automatically and do not need to be listed
# here explicitly.
#
THEORIES = itt/core fol

Then, in the top level of metaprl, invoke omake.

Now start MetaPRL, you can see the fol module has been enabled.

MetaPRL 0.9.6.5+  (Subversion rev unknown):
	build [Sun Sep 13 21:12:20 2020]
	on Costume-Party.local
	Uses VERBOSE Refiner_ds

Current directory: /
# ls ""
Root Theories Listing:
    Theory "base": Basic Meta-Theory
    Theory "fol": First-Order Logic
    Theory "itt_core": Computational Type Theory (Core Logic)
    Theory "support": MetaPRL Internal "Helper" Modules
    Theory "fs": Browse MetaPRL Source Code
end() : unit
#

You may copy files from fol to other directories such as tutorial to experiment with them.