Package mepk.kernel.internal

package mepk.kernel.internal

This package contains internal implementations for the concepts in the mepk.kernel package. They are not intended to be used directly.

Related Packages

Package	Description
mepk.kernel	This package implements the trusted kernel of MEPK.
mepk.kernel.util	This package contains utilities which are necessary for the kernel, but which are also useful outside of it.

Classes

Class	Description
Compose	A compose proof takes statements x, y, ..., each with hypotheses Hx1, Hx2, ... and conclusion Cx, ..., and a statement with exactly the same hypotheses Cx, Cy, ... and conclusion C: it 'applies' the latter statement, by constructing the statement with hypotheses Hx1, Hx2, ..., Hy1, Hy2, ..., and conclusion C.
Substitute	A substitution proof step takes a statement, and constructs a structurally similar statement by substituting one variable for a (typed) expression.
Weaken	A weakening proof step constructs a new statement by adding DVRs and/or hypotheses to an existing statement.