Package | Description |
---|---|
fmrisc.ProofNavigator.Syntax |
Modifier and Type | Class and Description |
---|---|
class |
ArrayTerm
Handling of array terms.
|
class |
ExistsFormula
Handling of universally quantified formulas.
|
class |
ForallFormula
Handling of universally quantified formulas.
|
class |
LambdaTerm
Handling of lambda terms.
|
Modifier and Type | Method and Description |
---|---|
abstract QuantifiedExpression |
QuantifiedExpression.construct(TypedIdentifier[] variables,
Expression base)
Construct quantified expression.
|
QuantifiedExpression |
ExistsFormula.construct(TypedIdentifier[] variables,
Expression base)
Construct quantified expression.
|
QuantifiedExpression |
LambdaTerm.construct(TypedIdentifier[] variables,
Expression base)
Construct quantified expression.
|
QuantifiedExpression |
ArrayTerm.construct(TypedIdentifier[] variables,
Expression base)
Construct quantified expression.
|
QuantifiedExpression |
ForallFormula.construct(TypedIdentifier[] variables,
Expression base)
Construct quantified expression.
|