Uses of Class
fmrisc.Semantics.Environment

Packages that use Environment

fmrisc.ProofNavigator
fmrisc.ProofNavigator.Commands
fmrisc.Proving
fmrisc.Semantics
fmrisc.Syntax

Uses of Environment in fmrisc.ProofNavigator

Methods in fmrisc.ProofNavigator that return Environment

static Environment	State.getEnvironment() get environment used by proof navigator
static Environment	State.getGlobal() get global environment of proof navigator

Methods in fmrisc.ProofNavigator with parameters of type Environment

static void

State.setEnvironment(Environment env) set environment used by proof navigator

Uses of Environment in fmrisc.ProofNavigator.Commands

Methods in fmrisc.ProofNavigator.Commands with parameters of type Environment

FormulaSymbol[]

Lemma.getSymbols(Environment env) Return symbols of formulas referenced in lemma.

Uses of Environment in fmrisc.Proving

Methods in fmrisc.Proving that return Environment

Environment

ProofState.getEnvironment() get environment of proof state

Methods in fmrisc.Proving with parameters of type Environment

void	ProofState.setEnvironment(Environment env) set environment of proof state

Constructors in fmrisc.Proving with parameters of type Environment

ProofState(Proof proof, Environment env, Expression goal, boolean autoSimplify)
construct a root state from a single goal and without assumptions

ProofState(ProofState parent, Environment env)
construct a proof state without path and formulas yet

Uses of Environment in fmrisc.Semantics

Methods in fmrisc.Semantics that return Environment

Environment	Environment.cloneGlobal() Create clone of global part of environment; the clone is a shallow copy (the symbols in the environment are not cloned).
Environment	FormulaSymbol.getEnvironment() Return environment of symbol (up to the point where the symbol was decld).

Methods in fmrisc.Semantics with parameters of type Environment

FormulaSymbol	FormulaTable.put(FormulaDeclIdentifier key, Expression formula, boolean axiom, Environment env) put formula in formula table
void	FormulaSymbol.setEnvironment(Environment env) Set environment of symbol (up to the point where the symbol was decld).
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 Environment in fmrisc.Syntax

Constructors in fmrisc.Syntax with parameters of type Environment

UniqueNameTable(Environment env)
Create name table such that no generated name conflicts with any value identifier in the given environment.