Package | Description |
---|---|
fmrisc.ProofNavigator.Syntax |
Modifier and Type | Class and Description |
---|---|
class |
AndFormula
Handling of conjunctions.
|
class |
ApplicationExpression
Handling of function and predicate applications.
|
class |
ArrayTerm
Handling of array terms.
|
class |
BinaryExpression
Abstract base class of binary expressions
|
class |
BitAndTerm
Handling of bit conjunctions.
|
class |
BitLogical
Bit logical constants.
|
class |
BitNotTerm
Handling of bit negations
|
class |
BitOrTerm
Handling of bit disjunctions.
|
class |
DividesTerm
Handling of quotients.
|
class |
EqualsFormula
Handling of equalities.
|
class |
EquivalentFormula
Handling of equivalences.
|
class |
ExistsFormula
Handling of universally quantified formulas.
|
class |
ForallFormula
Handling of universally quantified formulas.
|
class |
GreaterEqualFormula
Handling of greater-than-or-equal formulas.
|
class |
GreaterFormula
Handling of greater-than formulas.
|
class |
IfThenElseExpression
Handling of if-then-else expressions.
|
class |
ImpliesFormula
Handling of implications
|
class |
LambdaTerm
Handling of lambda terms.
|
class |
LessEqualFormula
Handling of less-than-or-equal formulas.
|
class |
LessFormula
Handling of less-than formulas.
|
class |
LetExpression
Handling of terms with local bindings.
|
class |
Logical
Logical constants.
|
class |
MinusTerm
Handling of differences.
|
class |
NegationTerm
Handling of negated (minus) terms
|
class |
NotEqualsFormula
Handling of conjunctions
|
class |
NotEquivalentFormula
Handling of conjunctions
|
class |
NotFormula
Handling of negations
|
class |
OrFormula
Handling of disjunctions.
|
class |
PlusTerm
Handling of binary sums.
|
class |
PowerTerm
Handling of power terms.
|
class |
QuantifiedExpression
Abstract base class of quantified expressions.
|
class |
RecordTerm
Handling of record terms.
|
class |
SelectionTerm
Handling of component access by index selections.
|
class |
TimesTerm
Handling of conjunctions
|
class |
TupleTerm
Handling of tuple terms.
|
class |
UnaryExpression
Abstract base class of unary expressions
|
class |
UpdateTerm
Handling of component updates by index selection.
|