Package mepk.builtin

package mepk.builtin

This package implements extensions on top of the mepk.kernel. The main entry point is TrustedProof. The code was carefully designed to make sure that Proof.verify() always succeeds for a TrustedProof; but in case of doubt you can always verify() that.

This package also contains a set of parsers in MEPKParsers.

Related Packages

Package	Description
mepk	This package implements MEPK, a minimal extensible proof kernel, with a Metamath/Ghilbert-like language.
mepk.builtin.internal	This package contains internal implementations for the concepts in the mepk.builtin package.
mepk.kernel	This package implements the trusted kernel of MEPK.

Class	Description
MEPKParseException	This exception indicates that a String could not be parsed to an Expression, a Statement, or a Set of Statements.
MEPKParsers	Parsers for expressions, etc.
TrustedProof	A trusted proof is a Proof which is built on the trusted kernel.
TrustedProof.Internal	An internal version of a TrustedProof.
Types	A helper class for easily creating a Map<String,String>, which maps variable names to type expressions.
Types.TypeMapBuilder	A HashMap<String,String> mapping variables to type expressions.