Uses of Class
fmrisc.Syntax.Identifier

Packages that use Identifier

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

Uses of Identifier in fmrisc.Communication

Methods in fmrisc.Communication that return Identifier

static Identifier	Store.toIdentifier(org.w3c.dom.Node node) Convert DOM node to identifier.
static Identifier	OpenMath.toIdentifier(nl.tue.win.riaca.openmath.lang.OMObject om) Convert OpenMath expression to identifier..

Methods in fmrisc.Communication with parameters of type Identifier

void	MathML.appendIdentifier(org.w3c.dom.Node parent, Identifier object) Convert identifier to DOM representation of HTML/MathML markup.

Uses of Identifier in fmrisc.ProofNavigator.Commands

Methods in fmrisc.ProofNavigator.Commands that return Identifier

Identifier

Prove.getIdent() get name of formula to be proved

Constructors in fmrisc.ProofNavigator.Commands with parameters of type Identifier

Expand(Identifier[] idents, java.lang.String[] labels)
Create an "expand" command.

FormulaC(Identifier ident)
Create a "formula" command.

Induction(Identifier var, java.lang.String label)
Create an "induction" command.

Lemma(Identifier[] idents)
Create a "lemma" command.

ProofC(Identifier ident)
Create a "proof" command.

Prove(Identifier ident)
create a prove command

StateC(java.lang.String label, Identifier ident)
Create a "state" command

TypeC(Identifier ident)
Create a "type" command.

ValueC(Identifier ident)
Create a "value" command.

Uses of Identifier in fmrisc.Proving

Methods in fmrisc.Proving with parameters of type Identifier

void	Proof.referenced(Identifier ident) Mark identifier as referenced in current proof.

Uses of Identifier in fmrisc.Proving.CVCL

Methods in fmrisc.Proving.CVCL with parameters of type Identifier

Expression

CVCLFormulaMask.getFormula(Identifier mask) Get formula associated to mask identifier

Uses of Identifier in fmrisc.Semantics

Methods in fmrisc.Semantics that return Identifier

Identifier	Symbol.getIdentifier() Get identifier associated to symbol.
Identifier	SymbolBase.getIdentifier() get identifier associated to symbol

Methods in fmrisc.Semantics with parameters of type Identifier

Expression	FormulaTable.getFormula(Identifier key) returns formula associated to key
FormulaSymbol	Environment.getFormulaSymbol(Identifier name) returns symbol associated to name (null, if none)
ValueSymbol	ValueTable.getSymbol(Identifier name) returns symbol associated to name (null, if none)
TypeSymbol	TypeTable.getSymbol(Identifier name) returns symbol associated to name (null, if none)
FormulaSymbol	FormulaTable.getSymbol(Identifier name) returns symbol associated to name (null, if none)
Type	Environment.getType(Identifier name) returns canonical type associated to key type equality implies pointer equality of types.
Type	TypeTable.getType(Identifier key) returns canonical type associated to key type equality implies pointer equality of types.
TypeSymbol	Environment.getTypeSymbol(Identifier name) returns type symbol associated to key
ValueSymbol	Environment.getValueSymbol(Identifier name) returns symbol associated to name (null, if none)

Constructors in fmrisc.Semantics with parameters of type Identifier

SymbolBase(Identifier ident)
construct symbol with given identifier

Uses of Identifier in fmrisc.Syntax

Subclasses of Identifier in fmrisc.Syntax

class	FormulaDeclIdentifier Handling of identifiers used in type declarations
class	Reference Handling of identifiers used in declarations
class	TypeDeclIdentifier Handling of identifiers used in type declarations
class	ValueDeclIdentifier Handling of identifiers used in value declarations

Methods in fmrisc.Syntax that return Identifier

Identifier	ValueDeclaration.getIdentifier() returns declaration name
Identifier	TypeDeclaration.getIdentifier() returns declaration name
Identifier	FormulaDeclaration.getIdentifier() returns declaration name
Identifier	Declaration.getIdentifier() Returns declaration name.