Modifier and Type | Method and Description |
---|---|
Identifier |
Prove.getIdent()
get name of formula to be proved
|
Constructor and Description |
---|
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.
|
Modifier and Type | Method and Description |
---|---|
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..
|
Modifier and Type | Method and Description |
---|---|
void |
MathML.appendIdentifier(org.w3c.dom.Node parent,
Identifier object)
Convert identifier to DOM representation of HTML/MathML markup.
|
Modifier and Type | Method and Description |
---|---|
void |
Proof.referenced(Identifier ident)
Mark identifier as referenced in current proof.
|
Modifier and Type | Method and Description |
---|---|
Expression |
CVCLFormulaMask.getFormula(Identifier mask)
Get formula associated to mask identifier
|
Modifier and Type | Method and Description |
---|---|
Identifier |
Symbol.getIdentifier()
Get identifier associated to symbol.
|
Identifier |
SymbolBase.getIdentifier()
get identifier associated to symbol
|
Modifier and Type | Method and Description |
---|---|
Expression |
FormulaTable.getFormula(Identifier key)
returns formula associated to key
|
FormulaSymbol |
Environment.getFormulaSymbol(Identifier name)
returns symbol associated to name (null, if none)
|
TypeSymbol |
TypeTable.getSymbol(Identifier name)
returns symbol associated to name (null, if none)
|
ValueSymbol |
ValueTable.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 |
TypeTable.getType(Identifier key)
returns canonical type associated to key
type equality implies pointer equality of types.
|
Type |
Environment.getType(Identifier name)
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)
|
Constructor and Description |
---|
SymbolBase(Identifier ident)
construct symbol with given identifier
|
Modifier and Type | Class and Description |
---|---|
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
|
Modifier and Type | Method and Description |
---|---|
Identifier |
ValueDeclaration.getIdentifier()
returns declaration name
|
Identifier |
Declaration.getIdentifier()
Returns declaration name.
|
Identifier |
FormulaDeclaration.getIdentifier()
returns declaration name
|
Identifier |
TypeDeclaration.getIdentifier()
returns declaration name
|