A B C D E F G H I J K L M N O P Q R S T U V W X _

T

TCC - Class in fmrisc.ProofNavigator.Commands

"tcc": print type checking conditions generated from last declaration.

TCC() - Constructor for class fmrisc.ProofNavigator.Commands.TCC

create a TCC command

tdeclaration() - Method in class fmrisc.Proving.CVCL.CVCLParser

tdeclaration0() - Method in class fmrisc.Proving.CVCL.CVCLParser

terminate() - Method in class fmrisc.Proving.CVCL.CVCL

Terminate prover instance.

terminate() - Method in interface fmrisc.Proving.Prover

Terminate prover instance.

TextInputStream - Class in fmrisc.ProofNavigator.SWT

Mapping of a Text widget to an InputStream object.

TextInputStream(Text, PrintWriter, Charset) - Constructor for class fmrisc.ProofNavigator.SWT.TextInputStream

Create an input stream from a Text widget.

TextOutputStream - Class in fmrisc.ProofNavigator.SWT

Mapping of an OutputStream object to a Text widget.

TextOutputStream(Text, Charset) - Constructor for class fmrisc.ProofNavigator.SWT.TextOutputStream

Create an output stream from a Text widget.

TIMES - Static variable in interface fmrisc.ProofNavigator.PNParserTokenTypes

TIMES - Static variable in interface fmrisc.Proving.CVCL.CVCLParserTokenTypes

timesTerm(Expression, Expression) - Static method in class fmrisc.Syntax.Construct

construct binary product with components base1 and base2

TimesTerm - Class in fmrisc.Syntax

Handling of conjunctions

TimesTerm(Expression, Expression) - Constructor for class fmrisc.Syntax.TimesTerm

construct binary product with components base1 and base2

toArray(Vector) - Static method in class fmrisc.Proving.Formula

converts vector v of Formula objects to array

toCommand(Element) - Static method in class fmrisc.ProofNavigator.Commands.CommandBase

Construct command from DOM representation.

toConjunction(Expression[]) - Static method in class fmrisc.Syntax.ASTUtil

Construct conjunction of sequence of formulas.

toCVCL(Expression) - Method in class fmrisc.Proving.CVCL.CVCL

return CVCL representation of expression

toDeclaration(Node) - Static method in class fmrisc.Communication.OMDoc

Convert OMDoc representation to declaration.

toDeclaration(Node) - Static method in class fmrisc.Communication.Store

Convert DOM node to declaration.

toDeclarationArray(Vector) - Static method in class fmrisc.Syntax.ASTUtil

converts vector v of Declaration objects to Declaration array

toDisjunction(Expression[]) - Static method in class fmrisc.Syntax.ASTUtil

Construct disjunction of sequence of formulas.

toExpression(OMObject) - Static method in class fmrisc.Communication.OpenMath

Convert OpenMath expression to AST.

toExpression(Node) - Static method in class fmrisc.Communication.Store

Convert DOM node to expression.

toExpressionArray(Vector) - Static method in class fmrisc.Syntax.ASTUtil

converts vector v of Expression objects to Expression array

toFormulaArray(Vector) - Static method in class fmrisc.Proving.ProofUtil

converts vector v of Formula objects to Formula array

toIdentifier(OMObject) - Static method in class fmrisc.Communication.OpenMath

Convert OpenMath expression to identifier..

toIdentifier(Node) - Static method in class fmrisc.Communication.Store

Convert DOM node to identifier.

toNode(Declaration) - Method in class fmrisc.Communication.OMDoc

Convert declaration to OMDoc representation in DOM format.

toNode(Document) - Method in interface fmrisc.ProofNavigator.Commands.Command

Convert proof command to external representation as a DOM node.

toNode(Document) - Method in class fmrisc.ProofNavigator.Commands.CommandBase

Convert proof command to external representation as a DOM node.

toNode(Document) - Method in class fmrisc.Proving.Proof

Convert proof to DOM node in denoted document.

toOpenMath(AST) - Static method in class fmrisc.Communication.OpenMath

Convert AST to OpenMath object.

Top - Class in fmrisc.ProofNavigator.SWT

The top panel of the GUI.

Top(Shell, int) - Constructor for class fmrisc.ProofNavigator.SWT.Top

Construct panel for denoted shell and with denoted style.

toProof(FormulaSymbol, Node) - Static method in class fmrisc.Proving.Proof

Construct skeleton proof from DOM representation.

toProofStateArray(Vector) - Static method in class fmrisc.Proving.ProofUtil

converts vector v of ProofState objects to ProofState array

toReferenceArray(Vector) - Static method in class fmrisc.Syntax.ASTUtil

converts vector v of Reference objects toarray

toSelectorArray(Vector) - Static method in class fmrisc.Syntax.ASTUtil

converts vector v of Selector objects to Selector array

toString() - Method in class fmrisc.ProofNavigator.Commands.CommandBase

returns string representation of tree

toString(AST) - Static method in class fmrisc.Proving.CVCL.CVCLPrinter

Convert abstract syntax tree to CVCL syntax.

toString() - Method in interface fmrisc.Syntax.AST

returns string representation of tree

toString() - Method in class fmrisc.Syntax.ASTBase

returns string representation of tree

toStringArray(Vector) - Static method in class fmrisc.Syntax.ASTUtil

converts vector v of String objects to String array

toType(OMObject) - Static method in class fmrisc.Communication.OpenMath

Convert OpenMath type to AST.

toType(Node) - Static method in class fmrisc.Communication.Store

Convert DOM node to type.

toTypeArray(Vector) - Static method in class fmrisc.Syntax.ASTUtil

converts vector v of Type objects to Type array

toTypeDeclarationArray(Vector) - Static method in class fmrisc.Syntax.ASTUtil

converts vector v of TypeDeclaration objects to TypeDeclaration array

toTypedIdentifierArray(Vector) - Static method in class fmrisc.Syntax.ASTUtil

converts vector v of TypedIdentifer objects to TypedIdentifier array

toValueDeclarationArray(Vector) - Static method in class fmrisc.Syntax.ASTUtil

converts vector v of ValueDeclaration objects to ValueDeclaration array

toValuedIdentifierArray(Vector) - Static method in class fmrisc.Syntax.ASTUtil

converts vector v of ValuedIdentifer objects to ValuedIdentifier array

tryHard(boolean) - Method in class fmrisc.Proving.CVCL.CVCL

Try hard to simplify (potentially timeconsuming).

tryHard(boolean) - Method in interface fmrisc.Proving.Prover

Try hard to simplify (potentially timeconsuming).

tupleTerm(Expression[]) - Static method in class fmrisc.Syntax.Construct

construct tuple term of base terms

TupleTerm - Class in fmrisc.Syntax

Handling of tuple terms.

TupleTerm(Expression[]) - Constructor for class fmrisc.Syntax.TupleTerm

construct tuple term of base terms

tupleType(Type[]) - Static method in class fmrisc.Syntax.Construct

construct tuple type with denoted base types.

TupleType - Class in fmrisc.Syntax

Handling of tuple types.

TupleType(Type[]) - Constructor for class fmrisc.Syntax.TupleType

construct record type with denoted base types.

Type - Interface in fmrisc.Syntax

Interface to types.

TypeAxiom - Class in fmrisc.ProofNavigator.Commands

The "typeaxiom" command: instantiate a quantified type axiom.

TypeAxiom(Expression, Expression[]) - Constructor for class fmrisc.ProofNavigator.Commands.TypeAxiom

Create an "typeaxiom" command.

TypeBase - Class in fmrisc.Syntax

Base class of type expressions.

TypeBase() - Constructor for class fmrisc.Syntax.TypeBase

TypeC - Class in fmrisc.ProofNavigator.Commands

Command "type": print value of type identifier.

TypeC(Identifier) - Constructor for class fmrisc.ProofNavigator.Commands.TypeC

Create a "type" command.

typeDeclaration(TypeDeclIdentifier, Type) - Static method in class fmrisc.Syntax.Construct

construct type declaration with denoted name and type.

TypeDeclaration - Class in fmrisc.Syntax

Handling of type declarations.

TypeDeclaration(TypeDeclIdentifier, Type) - Constructor for class fmrisc.Syntax.TypeDeclaration

construct type declaration with denoted name and type.

typeDeclIdentifier(String) - Static method in class fmrisc.Syntax.Construct

construct type declaration identifier with denoted name.

TypeDeclIdentifier - Class in fmrisc.Syntax

Handling of identifiers used in type declarations

TypeDeclIdentifier(String) - Constructor for class fmrisc.Syntax.TypeDeclIdentifier

construct identifier from name

typedIdentifier(ValueDeclIdentifier, Type) - Static method in class fmrisc.Syntax.Construct

construct typed identifier from identifier and type.

TypedIdentifier - Class in fmrisc.Syntax

Handling of typed identifiers.

TypedIdentifier(ValueDeclIdentifier, Type) - Constructor for class fmrisc.Syntax.TypedIdentifier

construct typed identifier from identifier and type.

typeExp() - Method in class fmrisc.ProofNavigator.PNParser

typeExp() - Method in class fmrisc.Proving.CVCL.CVCLParser

typeExpBase() - Method in class fmrisc.ProofNavigator.PNParser

typeExpBase() - Method in class fmrisc.Proving.CVCL.CVCLParser

TypeExpression - Class in fmrisc.Semantics

Pair of type and exp.

TypeExpression(Type, Expression) - Constructor for class fmrisc.Semantics.TypeExpression

Construct pair of type and exp

TypeSymbol - Class in fmrisc.Semantics

Symbols in TypeTable.

TypeSymbol(TypeDeclIdentifier) - Constructor for class fmrisc.Semantics.TypeSymbol

Construct type symbol from ident (type is set to null).

TypeTable - Class in fmrisc.Semantics

Type table for type checking.

TypeTable() - Constructor for class fmrisc.Semantics.TypeTable