TypedTLAPlus.Expression.toComputable — translates a checked TLA⁺ expression into its computable fragment (ComputableTLAPlus.Expression's own module doc has the full per-constructor rationale). Structurally mirrors TypedTLAPlus.Expression.traverse's own recursion, reattaching source positions the same way (@@ pos) — total on every constructor ComputableTLAPlus.Expression keeps, throwing ComputableError.notComputable on fnSet/recordSet, and .internalInvariantViolated on whatever else shouldn't be reachable here at all (an unbounded quantifier domain, a bare temporal/action construct, a pending mvar coercion) — see Typed2Computable/Errors.lean's own doc for why these stay one defense-in-depth case rather than a dedicated error each.

τ/Origin fields pass through unchanged: ComputableTLAPlus.Typ/.Origin are literal reuses of TypedTLAPlus.Typ/.Origin (Core/ComputableTLAPlus/Syntax.lean), not a second copy, so there's nothing to convert.

partial def TypedTLAPlus.Expression.toComputable {m : Type → Type} [Monad m] [MonadDiagnostic Empty ComputableError m] : Expression Typ → m (ComputableTLAPlus.Expression ComputableTLAPlus.Typ)

See the module doc above. partial: structural recursion isn't visibly decreasing to Lean here, same reason Expression.map/.traverse are partial (nested List/Option occurrences of Expression).