The shape of a TLA⁺ declaration/module, shared verbatim by CoreTLAPlus and TypedTLAPlus: each stage's Declaration/Module is identical except for which stage's Expression former it closes over. Parametrized here by that former (E) so the shape and its Functor/Traversable/Bifunctor/Bitraversable instances are defined once; each stage recovers its Declaration/Module via an abbrev over its Expression.

SurfaceTLAPlus does not reuse this type — its own Declaration/Module (Core/SurfaceTLAPlus/Syntax.lean) widen .function's binder list to admit the shared-domain/ tuple-pattern sugar Desugarer/TLAPlus.lean flattens down to this shape.

inductive Declaration (E : Type → Type) (α : Type) : Type

A top-level TLA⁺ declaration. RECURSIVE and module INSTANCE are not represented.

• constants {E : Type → Type} {α : Type} : List (String × α) → Declaration E α
• variables {E : Type → Type} {α : Type} : List (String × α) → Declaration E α
• assume {E : Type → Type} {α : Type} : E α → Declaration E α
• operator {E : Type → Type} {α : Type} : α → String → List (String × ℕ) → E α → Declaration E α

  An operator definition, optionally with higher-order arguments. Each parameter's Nat is its arity (0 for x, 3 for F(_, _, _), …).

• function {E : Type → Type} {α : Type} : α → String → List (String × E α) → E α → Declaration E α

  A function definition, with an explicit domain for every argument.

@[implicit_reducible]

instance instReprDeclaration {E : Type → Type} {α : Type} [Repr α] [Repr (E α)] : Repr (Declaration E α)

Hand-written since deriving Repr can't discharge the higher-kinded Repr (E α) obligation.

Equations

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

@[implicit_reducible]

instance instFunctorDeclaration {E : Type → Type} [Functor E] : Functor (Declaration E)

Equations

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

@[implicit_reducible]

instance instTraversableDeclaration {E : Type → Type} [Traversable E] : Traversable (Declaration E)

Equations

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

structure Module (E : Type → Type) (α β : Type) : Type

A TLA⁺ module, EXTENDS-list and all, wrapping the embedded (Distributed) PlusCal algorithm at whatever α the caller instantiates it at — kept abstract to avoid a cyclic import between the TLA⁺ and PlusCal Core ASTs. Each stage recovers its Module via an abbrev over its Expression (SurfaceTLAPlus.Module, CoreTLAPlus.Module, TypedTLAPlus.Module). Dot-called extension methods under a stage's Module namespace (mod.runChecker, mod.checkWellFormed, …) become qualified calls rather than method calls: generalized field notation resolves through the abbrev's full unfold, landing on this shared type instead of the stage's (nonexistent) namespace.

• name : String
• extends : List String
• declarations₁ : List (Declaration E β)
• pcalAlgorithm : Option α
• declarations₂ : List (Declaration E β)

@[implicit_reducible]

instance instInhabitedModule {a✝ : Type → Type} {a✝¹ a✝² : Type} : Inhabited (Module a✝ a✝¹ a✝²)

Equations

• instInhabitedModule = { default := instInhabitedModule.default }

@[implicit_reducible]

instance instReprModule {E : Type → Type} {α β : Type} [Repr α] [Repr β] [Repr (E β)] : Repr (Module E α β)

Hand-written, same reason as Declaration's Repr instance above.

Equations

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

@[implicit_reducible]

instance instBifunctorModuleOfFunctor {E : Type → Type} [Functor E] : Bifunctor (Module E)

@@ posOf m, for the same reason SurfacePlusCal.Process/.Algorithm's instances carry it: mapping a module rebuilds the structure, and a rebuilt node that isn't re-registered has no position of its own — posOf then answers for it with whatever unrelated value last occupied that address (Common/Position.lean). Annotation resolution alone maps every module once (CommentAnnotation → Annotation), and SurfaceTLAPlus.Module.desugar reads the result's position.

Equations

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

@[implicit_reducible]

instance instBitraversableModuleOfTraversable {E : Type → Type} [Traversable E] : Bitraversable (Module E)

Equations

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