Uses of Interface
fmrisc.ProgramExplorer.Syntax.Logic.ValueDefinition

Packages that use ValueDefinition

Package	Description
fmrisc.ProgramExplorer.Parser
fmrisc.ProgramExplorer.Proving
fmrisc.ProgramExplorer.Syntax.Logic

Uses of ValueDefinition in fmrisc.ProgramExplorer.Parser

Methods in fmrisc.ProgramExplorer.Parser that return ValueDefinition

Modifier and Type	Method and Description
ValueDefinition	SpecLangParser.vdefinition()

Uses of ValueDefinition in fmrisc.ProgramExplorer.Proving

Methods in fmrisc.ProgramExplorer.Proving with parameters of type ValueDefinition

Modifier and Type	Method and Description
ValueDeclaration[]	ProofNavigator.translateValueDefs(ValueDefinition[] defs) Translate value definitions.

Uses of ValueDefinition in fmrisc.ProgramExplorer.Syntax.Logic

Classes in fmrisc.ProgramExplorer.Syntax.Logic that implement ValueDefinition

Modifier and Type	Class and Description
class	ValueDeclarationInitialized The declaration of a value with initialization.
class	ValueDefinitionClass The definition of a value.

Methods in fmrisc.ProgramExplorer.Syntax.Logic that return ValueDefinition

Modifier and Type	Method and Description
ValueDefinition[]	LetFormula.getDefinitions() Get definitions.
ValueDefinition[]	LetTerm.getDefinitions() Get definitions.

Methods in fmrisc.ProgramExplorer.Syntax.Logic with parameters of type ValueDefinition

Modifier and Type	Method and Description
static LetFormula	LetFormula.construct(ValueDefinition[] d, Formula b) Construct formula with local value definitions.
static LetTerm	LetTerm.construct(ValueDefinition[] d, Term b) Construct term with local value definitions.