Coercion — a term-level witness of <:, realized as closed structural data, not an opaque Expr → Expr closure. Lives in Core/ (not Elaborator/) so CorePlusCal.Statement.receive can carry a Coercion field without Core/ depending on Elaborator/. Elaborator/ Subtyping.lean owns everything about Coercion (the subtyping judgment, every coercion built from one); this file only owns the type itself, its discharge (Coercion.apply), and its Repr instance.

Data rather than a closure because a receive statement's coercion (Core/GuardedPlusCal/ Syntax.lean) must survive past Typed2Computable's type change (TypedTLAPlus.Expression → ComputableTLAPlus.Expression) and discharge against the later type — a closure fixed at one concrete Expr type can't cross that boundary. Each constructor mirrors one of Elaborator/ Subtyping.lean's structural <: rules (or tryAxioms's non-structural ones), carrying the type indices, field names, and nested sub-Coercions that rule's discharge needs, plus any fresh binder name (x/y/i) generated via MonadFresh at construction time — baked in once, since a name fresh at construction stays fresh at discharge.

Two structural recursions consume this data, one per concrete expression type: Coercion.apply (below) and Coercion.applyComputable (Core/ComputableTLAPlus/Coercion.lean).

Repr Coercion is a placeholder: -d dump-typecheck renders any receive's coercion as the literal string "<coercion>".

@[reducible, inline]

abbrev TypedTLAPlus.Expr : Type

Checked TLA⁺ expressions at the checker's own output type — what a Coercion transforms.

Equations

• TypedTLAPlus.Expr = TypedTLAPlus.Expression TypedTLAPlus.Typ

inductive TypedTLAPlus.Coercion : Type

A coercion, witnessing τ <: τ' at the term level. .id is its own constructor rather than folded into a general case, so structural subtyping rules can cheaply detect "nothing to wrap" by pattern matching alone.

• id : Coercion

  No wrapping needed — the source expression is already of the target type as-is.

• strToSeq : Coercion

  Str <: Seq(Int) — StrToSeq(e), the sequence of the string's Unicode code points. An intrinsic (Origin.intrinsic) rather than a member of Sequences: real TLA⁺ has no such operator, and only a coercion ever builds this node, so binding a name for it in builtinContext would invent surface syntax nothing needs.

• seqToFun (τ : Typ) (i : String) : Coercion

  Seq(τ) <: Int → τ — [i ∈ 1..Len(e) ↦ e[i]]. i a fresh name chosen at construction.

• bagToFun (τ : Typ) (i : String) : Coercion

  Bag(τ) <: τ → Int — [i ∈ Bags!BagToSet(e) ↦ Bags!CopiesIn(i, e)]. i a fresh name chosen at construction.

• tupleToSeq (n : ℕ) (τ : Typ) (hn : 0 < n) : Coercion

  ⟨τ,...,τ⟩ <: Seq(τ) (uniform tuple only) — a tuple's arity n is static, so discharge is just a literal .seq of the n projected components. hn — a tuple is non-empty, so the discharged .seq evaluates its source at least once (needed for evalCoerce, whose right-hand side asserts the source has a value at all).

• set (x : String) (τ τ' : Typ) (c : Coercion) : Coercion

  Set(τ) <: Set(τ') — {coerce(x) : x ∈ e}. x a fresh binder name. τ' is carried alongside the source τ because the .map' this discharges to records its codomain, and the coerced body's type is exactly τ'.

• tuple (coes : List Coercion) (τs τs' : List Typ) : Coercion

  ⟨τ₁,...,τₙ⟩ <: ⟨τ₁',...,τₙ'⟩ — a new literal tuple, each component projected out of the source (tuples being encoded as unary functions from naturals) and coerced. τs is the source component list, needed because each projection discharges to a .fnCall, which records the type of its head — here the source tuple.

• record (fields : List (String × Coercion × Typ)) : Coercion

  [x₁:τ₁,...] <: [x₁:τ₁',...] — a new literal record, each field projected out of the source and coerced.

• function (x y : String) (dom rng dom' rng' : Typ) (cDom cRng : Coercion) : Coercion

  τ₁ → τ₂ <: τ₁' → τ₂' via a CHOOSE-based domain remap. x/y fresh binder names. rng' is carried for the same reason set carries τ': the .fn this discharges to records its codomain, which is the target range, not the source's.

• comp (c₁ c₂ : Coercion) : Coercion

  Sequential composition — discharge c₁ then c₂ on the result. Realizes <:'s transitivity for tryAxioms' chained-axiom case (e.g. Str <: Seq(Int) <: Int → Int).

partial def TypedTLAPlus.Coercion.apply (c : Coercion) (e : Expr) : Expr

Apply a coercion to an already-elaborated expression.

Every node built here is synthesized — none of it has source text of its own — but all of it stands for the coerced expression e, so all of it is registered at e's own span. Leaving a synthesized node unregistered is not neutral: posOf cannot tell "never registered" from "registered by something now dead" and answers with an unrelated node's span (Common/Position.lean). A coercion inserted by subtyping can wrap most of an expression, so skipping this loses positions across whole subtrees.

@[implicit_reducible]

instance TypedTLAPlus.instReprCoercion : Repr Coercion

A placeholder rendering (module doc).

Equations

• TypedTLAPlus.instReprCoercion = { reprPrec := fun (x : TypedTLAPlus.Coercion) (x_1 : ℕ) => Std.Format.text "<coercion>" }