Uses of Package
fmrisc.Syntax

Packages that use fmrisc.Syntax

fmrisc.Communication
fmrisc.ProofNavigator
fmrisc.ProofNavigator.Commands
fmrisc.Proving
fmrisc.Proving.CVCL
fmrisc.Semantics
fmrisc.Syntax

Classes in fmrisc.Syntax used by fmrisc.Communication

AST
Interface to abstract syntax trees.

Declaration
Interface for declarations.

Expression
Interface to expressions (terms and formulas).

Identifier
Handling of identifiers.

Type
Interface to types.

TypedIdentifier
Handling of typed identifiers.

Classes in fmrisc.Syntax used by fmrisc.ProofNavigator

Declaration
Interface for declarations.

Expression
Interface to expressions (terms and formulas).

Type
Interface to types.

TypedIdentifier
Handling of typed identifiers.

ValueDeclaration
Handling of value declarations.

Classes in fmrisc.Syntax used by fmrisc.ProofNavigator.Commands

Declaration
Interface for declarations.

Expression
Interface to expressions (terms and formulas).

Identifier
Handling of identifiers.

Classes in fmrisc.Syntax used by fmrisc.Proving

ASTVisitor
Interface to visitor of abstract syntax trees.

ASTVisitorBase
Base class of visitors of abstract syntax trees.

Declaration
Interface for declarations.

Expression
Interface to expressions (terms and formulas).

Identifier
Handling of identifiers.

UniqueNameTable
Table used to create unique names from given names.

ValueDeclIdentifier
Handling of identifiers used in value declarations

Classes in fmrisc.Syntax used by fmrisc.Proving.CVCL

AST
Interface to abstract syntax trees.

Declaration
Interface for declarations.

Expression
Interface to expressions (terms and formulas).

Identifier
Handling of identifiers.

Type
Interface to types.

TypeDeclaration
Handling of type declarations.

TypedIdentifier
Handling of typed identifiers.

ValueDeclaration
Handling of value declarations.

ValueDeclIdentifier
Handling of identifiers used in value declarations

Classes in fmrisc.Syntax used by fmrisc.Semantics

ASTVisitor
Interface to visitor of abstract syntax trees.

ASTVisitorBase
Base class of visitors of abstract syntax trees.

Expression
Interface to expressions (terms and formulas).

FormulaDeclaration
Handling of type declarations.

FormulaDeclIdentifier
Handling of identifiers used in type declarations

Identifier
Handling of identifiers.

Type
Interface to types.

TypeDeclaration
Handling of type declarations.

TypeDeclIdentifier
Handling of identifiers used in type declarations

TypedIdentifier
Handling of typed identifiers.

ValueDeclaration
Handling of value declarations.

ValueDeclIdentifier
Handling of identifiers used in value declarations

Classes in fmrisc.Syntax used by fmrisc.Syntax

AndFormula
Handling of conjunctions.

ApplicationExpression
Handling of function and predicate applications.

ArrayTerm
Handling of array terms.

ArrayType
Handling of array types.

AST
Interface to abstract syntax trees.

ASTBase
Base class of abstract syntax trees.

ASTVisitor
Interface to visitor of abstract syntax trees.

AtomicType
Handling of atomic types.

AxiomDeclaration
Handling of type declarations.

BinaryExpression
Abstract base class of binary expressions

Declaration
Interface for declarations.

DeclarationBase
Base class of type expressions.

DividesTerm
Handling of quotients.

EqualsFormula
Handling of equalities.

EquivalentFormula
Handling of equivalences.

ExistsFormula
Handling of universally quantified formulas.

Expression
Interface to expressions (terms and formulas).

ExpressionBase
Base class of all expressions (terms and formulas)

ForallFormula
Handling of universally quantified formulas.

FormulaDeclaration
Handling of type declarations.

FormulaDeclIdentifier
Handling of identifiers used in type declarations

FunctionType
Handling of function type expressions

GreaterEqualFormula
Handling of greater-than-or-equal formulas.

GreaterFormula
Handling of greater-than formulas.

Identifier
Handling of identifiers.

IfThenElseExpression
Handling of if-then-else expressions.

ImpliesFormula
Handling of implications

LambdaTerm
Handling of lambda terms.

LessEqualFormula
Handling of less-than-or-equal formulas.

LessFormula
Handling of less-than formulas.

LetExpression
Handling of terms with local bindings.

LetType
Handling of terms with local bindings.

Logical
Logical constants.

MinusTerm
Handling of differences.

NegationTerm
Handling of negated (minus) terms

NotEqualsFormula
Handling of conjunctions

NotEquivalentFormula
Handling of conjunctions

NotFormula
Handling of negations

Number
Handling of numbers.

OrFormula
Handling of disjunctions.

PlusTerm
Handling of binary sums.

PowerTerm
Handling of power terms.

QuantifiedExpression
Abstract base class of quantified expressions.

RecordTerm
Handling of record terms.

RecordType
Handling of record types.

Reference
Handling of identifiers used in declarations

SelectionTerm
Handling of component access by index selections.

Selector
Interface to selectors.

SelectorBase
Base class of selector expressions.

SelectorIdentifier
Identifier as selector.

SelectorIndex
General index expression as selector.

SelectorNumber
Number as selector.

SubrangeType
Subranges of integers.

SubType
Predicated subtypes.

TimesTerm
Handling of conjunctions

TupleTerm
Handling of tuple terms.

TupleType
Handling of tuple types.

Type
Interface to types.

TypeBase
Base class of type expressions.

TypeDeclaration
Handling of type declarations.

TypeDeclIdentifier
Handling of identifiers used in type declarations

TypedIdentifier
Handling of typed identifiers.

UnaryExpression
Abstract base class of unary expressions

UniqueNameTable
Table used to create unique names from given names.

UpdateTerm
Handling of component updates by index selection.

ValueDeclaration
Handling of value declarations.

ValueDeclIdentifier
Handling of identifiers used in value declarations

ValuedIdentifier
Handling of identifier with value