Documentation

Core.TypedTLAPlus.Builtins

The single shared table of builtin operators — every name builtinContext (Elaborator/Declarations.lean) and builtinModules (Driver/Builtins.lean) bind, plus the coercion-only StrToSeq neither binds, keyed by (Origin, name). Pure data with no Driver/Elaborator dependency, so any pass downstream of type checking can recognize a builtin call without re-deriving its own string list.

This is the one place the name↔operator wiring is written down: the reserved-temporal-action check and Typed2Computable's "is this builtin computable?" question both read it from here.

One constructor per literal builtin rather than a lighter category-tagged table: gives exhaustiveness-checked matches to every downstream consumer, at the cost of hand-duplicating each name a third time here.

source
inductive TypedTLAPlus.BuiltinOp :
Type

One constructor per name builtinContext/builtinModules bind. Naming mirrors each operator's own TLA⁺ role, not its surface spelling (eq for =, cup for \cup, …) — see builtinOpOf? for the spelling↔constructor table itself.

Instances For
    source
    def TypedTLAPlus.instReprBuiltinOp.repr :
    BuiltinOp → ℕ → Std.Format
    Equations
    • One or more equations did not get rendered due to their size.
    Instances For
      source
      @[implicit_reducible]
      instance TypedTLAPlus.instReprBuiltinOp :
      Repr BuiltinOp
      Equations
      source
      @[implicit_reducible]
      instance TypedTLAPlus.instInhabitedBuiltinOp :
      Inhabited BuiltinOp
      Equations
      source
      @[implicit_reducible]
      instance TypedTLAPlus.instBEqBuiltinOp :
      BEq BuiltinOp
      Equations
      source
      def TypedTLAPlus.instBEqBuiltinOp.beq :
      BuiltinOp → BuiltinOp → Bool
      Equations
      Instances For
        source
        @[implicit_reducible]
        instance TypedTLAPlus.instDecidableEqBuiltinOp :
        DecidableEq BuiltinOp
        Equations
        source
        def TypedTLAPlus.builtinOpOf? :
        Origin → Option BuiltinOp

        The name↔operator table itself, one arm per BuiltinOp constructor (exhaustiveness-checked by the compiler — a new BuiltinOp constructor with no arm here is a build error, not a silent gap). none for any Origin not bound by builtinContext/builtinModules.

        Equations
        Instances For
          source
          theorem TypedTLAPlus.builtinOpOf?_eq_natSet {o : Origin} :
          builtinOpOf? o = some BuiltinOp.natSet ↔ o = Origin.module "Naturals" "Nat"

          builtinOpOf? picks out Nat only at Naturals!Nat.

          source
          theorem TypedTLAPlus.builtinOpOf?_eq_intSet {o : Origin} :
          builtinOpOf? o = some BuiltinOp.intSet ↔ o = Origin.module "Integers" "Int"

          builtinOpOf? picks out Int only at Integers!Int.

          source
          def TypedTLAPlus.Expression.recognizeBuiltin? {α : Type} :
          Expression α → Option (BuiltinOp × List (Expression α))

          Recognizes e as a builtin call — .opCall (.var _ origin) args where origin hits builtinOpOf? — returning the operator and its argument list. none for anything else, including a call to a resolved-but-non-builtin operator/function.

          Equations
          Instances For
            source
            def TypedTLAPlus.reservedTemporalActionNames :
            List String

            The eight reserved temporal/action operator spellings real TLA⁺ core syntax carries, banned outright by bare name in WellFormedness/Restrictions.lean's check 3 regardless of whether the name resolves to anything (a reserved name can never be shadowed by a user declaration, so an origin-agnostic check is exact). ^+/^*/^# have no typing rule and so no BuiltinOp constructor above — genuinely unbound, unlike the other five, which double as real builtinOpOf? entries (.enabled, .unchanged, .always, .eventually, .prime). Kept as a separate list rather than derived from builtinOpOf?, since the two overlap but aren't the same.

            Equations
            Instances For