Uses of Class
fmrisc.Syntax.TypedIdentifier

Packages that use TypedIdentifier

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

Uses of TypedIdentifier in fmrisc.Communication

Methods in fmrisc.Communication with parameters of type TypedIdentifier

void	MathML.appendTypedIdentifier(org.w3c.dom.Node parent, TypedIdentifier object) Convert typed identifier to DOM representation of HTML/MathML markup.
void	PrettyMathML.appendTypedIdentifier(org.w3c.dom.Node parent, TypedIdentifier object) Convert typed identifier to DOM representation of HTML/MathML markup.

Uses of TypedIdentifier in fmrisc.ProofNavigator

Methods in fmrisc.ProofNavigator that return TypedIdentifier

TypedIdentifier[]

PNParser.paramList()

Uses of TypedIdentifier in fmrisc.Proving.CVCL

Methods in fmrisc.Proving.CVCL that return TypedIdentifier

TypedIdentifier[]

CVCLParser.paramList()

Uses of TypedIdentifier in fmrisc.Semantics

Methods in fmrisc.Semantics with parameters of type TypedIdentifier

boolean	Environment.putVariables(TypedIdentifier[] vars) put variables into environment
static void	Checking.simplifyNames(TypedIdentifier[] vars, Environment env, Expression exp) Simplify names of local variables to their base names if no name capture can occur.

Uses of TypedIdentifier in fmrisc.Syntax

Methods in fmrisc.Syntax that return TypedIdentifier

TypedIdentifier[]	RecordType.getBase() returns base types
TypedIdentifier[]	QuantifiedExpression.getVariables() get quantified variables
TypedIdentifier	TypedIdentifier.instantiate() create instantiated copy of identifier
static TypedIdentifier[]	ASTUtil.toTypedIdentifierArray(java.util.Vector v) converts vector v of TypedIdentifer objects to TypedIdentifier array
static TypedIdentifier	Construct.typedIdentifier(ValueDeclIdentifier identifier, Type type) construct typed identifier from identifier and type.

Methods in fmrisc.Syntax with parameters of type TypedIdentifier

static ArrayTerm	Construct.arrayTerm(TypedIdentifier[] variables, Expression base) construct array term of variables and base term
QuantifiedExpression	ExistsFormula.construct(TypedIdentifier[] variables, Expression base) Construct quantified expression.
QuantifiedExpression	LambdaTerm.construct(TypedIdentifier[] variables, Expression base) Construct quantified expression.
abstract QuantifiedExpression	QuantifiedExpression.construct(TypedIdentifier[] variables, Expression base) Construct quantified expression.
QuantifiedExpression	ForallFormula.construct(TypedIdentifier[] variables, Expression base) Construct quantified expression.
QuantifiedExpression	ArrayTerm.construct(TypedIdentifier[] variables, Expression base) Construct quantified expression.
static ExistsFormula	Construct.existsFormula(TypedIdentifier[] variables, Expression base) construct existentially quantifed formula of variables and base formula
static ForallFormula	Construct.forallFormula(TypedIdentifier[] variables, Expression base) construct universally quantifed formula of variables and base formula
static LambdaTerm	Construct.lambdaTerm(TypedIdentifier[] variables, Expression base) construct lambda term of variables and base term
static RecordType	Construct.recordType(TypedIdentifier[] base) construct record type with denoted base types.
void	TypedIdentifier.setSubstitution(TypedIdentifier substitution) set substitution expression for instantiation

Constructors in fmrisc.Syntax with parameters of type TypedIdentifier

ArrayTerm(TypedIdentifier[] variables, Expression base)
construct array term of variables and base term

ExistsFormula(TypedIdentifier[] variables, Expression base)
construct exists formula of variables and base formula

ForallFormula(TypedIdentifier[] variables, Expression base)
construct forall formula of variables and base formula

LambdaTerm(TypedIdentifier[] variables, Expression base)
construct lambda term of variables and base term

QuantifiedExpression(java.lang.String quantifier, TypedIdentifier[] variables, Expression base)
constructs quantified expression from quantifier, variables, and base

RecordType(TypedIdentifier[] base)
construct record type