Uses of Class
mepk.kernel.Expression

Packages that use Expression

Package	Description
mepk.builtin	This package implements extensions on top of the mepk.kernel.
mepk.kernel	This package implements the trusted kernel of MEPK.
mepk.kernel.internal	This package contains internal implementations for the concepts in the mepk.kernel package.

Uses of Expression in mepk.builtin

Methods in mepk.builtin that return Expression

Modifier and Type	Method	Description
static Expression	MEPKParsers.Expr(String expressionAsString)	Parse the given expression string (in "Ghilbert format") to an Expression instance.

Uses of Expression in mepk.kernel

Methods in mepk.kernel that return Expression

Modifier and Type	Method	Description
static Expression	Expression.App(String constantName, Expression... subexpressions)	Create an application of a constant to a list of subexpressions.
static Expression	Expression.AppV(String constantName, String... variableNames)	Create an application of a constant to a list of variable names.
Expression	App.expand(Abbreviation abbreviation, StatementAbbrExpState accu, Expression.Internal.Wrapper wrapper)
Expression	Expression.expand(Abbreviation abbreviation, StatementAbbrExpState accu)	Create a new expression by expanding all instances of the given abbreviation, and collect all conditions in accu.
Expression	Expression.Internal.expand(Abbreviation abbreviation, StatementAbbrExpState accu, Expression.Internal.Wrapper wrapper)	Create a new expression by expanding all instances of the given abbreviation, and collect all conditions in accu.
Expression	Var.expand(Abbreviation abbreviation, StatementAbbrExpState accu, Expression.Internal.Wrapper wrapper)
Expression	Statement.getConclusion()	Returns the conclusion of this statement.
Expression	Abbreviation.getExpansion()	Returns the expansion of the abbreviation.
Expression	App.substitute(String varName, Expression.Internal replacement, Expression.Internal.Wrapper wrapper)
Expression	Expression.Internal.substitute(String varName, Expression.Internal replacement, Expression.Internal.Wrapper wrapper)	Create a new internal expression by replacing a variable by an internal expression.
Expression	Expression.substitute(String varName, Expression replacement)	Create a new expression by replacing a variable by an expression.
Expression	Var.substitute(String varName, Expression.Internal replacement, Expression.Internal.Wrapper wrapper)
static Expression	Expression.Type(String varName, String typeName)	Create a new expression saying 'this variable has that type'.
static Expression	Expression.Type(Expression expr, String typeName)	Create a new expression saying 'this expression has that type'.
static Expression	Expression.Var(String name)	Create a variable expression.
Expression	Expression.Internal.Wrapper.wrap(Expression.Internal internalExpression)	Wrap the given internal expression.

Methods in mepk.kernel that return types with arguments of type Expression

Modifier and Type	Method	Description
Collection<? extends Expression>	Statement.getHypotheses()	Returns the hypotheses of this statement.
List<Expression>	App.getSubexpressions()	Returns the subexpressions of this constant-application expression.

Methods in mepk.kernel with parameters of type Expression

Modifier and Type	Method	Description
static Expression	Expression.App(String constantName, Expression... subexpressions)	Create an application of a constant to a list of subexpressions.
static Statement	Statement.Stat(List<Expression> hypotheses, Expression conclusion)	Create a new instance with an empty set of DVRs.
static Statement	Statement.Stat(DVRSet dvrs, List<Expression> hypotheses, Expression conclusion)	Create a new instance.
Expression	Expression.substitute(String varName, Expression replacement)	Create a new expression by replacing a variable by an expression.
Statement	Statement.substitute(String varName, Expression replacement, Map<String,String> typesOfNewVars)	Create a new statement, by replacing one variable in this statement by an expression, and optionally adding type expressions (to make resulting statement type-correct).
static ProofStep	ProofStep.Substitute(Statement statement, String varName, Expression replacement, Map<String,String> typesOfNewVars)	Create a substitution proof step, which takes a statement s and a substitution, and constructs (grounds) the statement resulting from the substitution.
static Expression	Expression.Type(Expression expr, String typeName)	Create a new expression saying 'this expression has that type'.
Statement	Statement.weaken(DVRSet addedDVRs, Expression... addedHypotheses)	Create a new statement, by adding hypotheses and DVRs to this statement.
static ProofStep	ProofStep.Weaken(Statement statement, DVRSet addedDVRs, Expression... addedHypotheses)	Create a weakening proof step, which takes a statement and adds hypotheses and DVRs.

Method parameters in mepk.kernel with type arguments of type Expression

Modifier and Type	Method	Description
static Statement	Statement.Stat(List<Expression> hypotheses, Expression conclusion)	Create a new instance with an empty set of DVRs.
static Statement	Statement.Stat(DVRSet dvrs, List<Expression> hypotheses, Expression conclusion)	Create a new instance.

Constructors in mepk.kernel with parameters of type Expression

Modifier	Constructor	Description
	Abbreviation(Expression abbreviation, Expression expansion, Expression... conditions)	Create a new abbreviation.

Uses of Expression in mepk.kernel.internal

Constructors in mepk.kernel.internal with parameters of type Expression

Modifier	Constructor	Description
	Substitute(Statement statement, String varName, Expression replacement, Map<String,String> typesOfNewVars)	Create an instance.
	Weaken(Statement statement, DVRSet addedDVRs, Expression... addedHypotheses)	Create an instance.