CorePlusCal.WellScoped, a Prop. Same scope-class shape as the executable check (TypedPlusCal.Algorithm.checkWellScoped), stated over the pre-Elaborator CorePlusCal.Algorithm: it is the form a preservation lemma is stated against, not something the executable check invokes.

def CorePlusCal.Declarations.names {α β : Type} (d : Declarations α β) : List String

Every name a Declarations value binds — the Prop-side counterpart of TypedPlusCal.Declarations.namesWithPos, with no position (irrelevant to a Prop).

Equations

• One or more equations did not get rendered due to their size.

partial def CorePlusCal.Statement.WellScopedIn {α β : Type} {b : Bool} (inScope : List String) : Statement α β b → Prop

s introduces no shadowing/duplicate name, given inScope already holds — the Prop counterpart of TypedPlusCal.Statement.checkWellScoped.

partial def CorePlusCal.Block.WellScopedIn {α β : Type} {b : Bool} (inScope : List String) (B : Block α β b) : Prop

partial def CorePlusCal.Branches.WellScopedIn {α β : Type} {b : Bool} (inScope : List String) : Branches α β b → Prop

def CorePlusCal.WellScoped {α β : Type} (algo : Algorithm α β) : Prop

p has no duplicate name in any scope, and no name shadows an enclosing scope's — the Prop counterpart of TypedPlusCal.Algorithm.checkWellScoped, over the pre-Elaborator CorePlusCal.Algorithm.

Equations

• One or more equations did not get rendered due to their size.