Building the Ord dictionary a TLA⁺ type is ordered by.

The runtime represents ordering as a value — tlaplus.Ord[T] is a struct of two functions, Eq and Lt — rather than as an interface a type implements. Go has no conditional method sets, so Set[T] could not declare a comparison that calls T's; a dictionary sidesteps that, keeps every container [T any], and makes nesting ordinary composition (Set[Set[Int]]'s dictionary is SetOrd(SetOrd(IntOrd))). Every runtime operation that compares takes one.

So ordDict is a second fold over Typ, mirroring compileTyp constructor for constructor: one produces the type, the other the dictionary ordering it. The two must agree, since a Set does not record which dictionary built it and every operation on it has to be handed the same one — that they are derived from the same Typ is what guarantees it.

Three kinds of answer:

• Closed expressions, for everything built out of the runtime's own types: a package-level value (tlaplus.IntOrd) or a constructor applied to its components (tlaplus.SetOrd(…)).
• A literal, for records and tuples. These compile to anonymous Go structs, which can carry no methods — but a dictionary needs none, so the comparison functions are written out inline at each use. This is what removed the need for generated named types and a mangling scheme; Go identifies anonymous struct types structurally, so two identically-shaped records are already the same type, and compileTyp's field sorting is what makes the shapes coincide.
• A parameter, for a rigid type variable, bound by the enclosing definition.

Rejected wholesale: .operator. Operators compile to Go funcs, which have no equality at all, and TLA⁺ operators are not values, so one can never appear inside a set, a sequence, a record or a function's domain.

partial def Network2Go.ordDict {m : Type → Type} [Monad m] [MonadDiagnostic Empty N2GError m] : ComputableTLAPlus.Typ → m ComputableGo.Expression

The dictionary ordering values of a TLA⁺ type.

Fails on exactly the types that have no ordering and cannot need one — see the module doc.

partial def Network2Go.structDict {m : Type → Type} [Monad m] [MonadDiagnostic Empty N2GError m] (goτ : Go.Typ) (fields : List (String × ComputableTLAPlus.Typ)) : m ComputableGo.Expression

The dictionary for a record or a tuple, as a literal beside the anonymous struct type it orders.

Equality is componentwise; the order is lexicographic in the struct's own field order. Both are written against goτ, which the caller has already computed, so that the type is spelled identically in the literal's type argument and in both function signatures — Go compares anonymous struct types structurally, and a mismatch would not be a type error, just a different type.

partial def Network2Go.Typ.typeVars : ComputableTLAPlus.Typ → List String

The rigid type variables a type mentions, in first-occurrence order — the type parameters, and hence the dictionary parameters, a definition of that type has to bind; a type variable is propagated to the nearest enclosing function definition.