parks-a-dispatch-off-a-symbol.yaml

# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com
# SPDX-License-Identifier: MIT
---
# yamllint disable rule:line-length
# A λ binding naming a symbol rather than a name, which is what a value nobody
# worked out looks like: ⟦ λ ⤍ 𝜎1 ⟧. Dispatching an attribute off it asks 𝕄 to
# reduce it, 'ml' fires 𝔼 on the target, and before #1287 𝔼 refused the
# formation outright — a 'userError' nothing catches, so the whole run died on
# the first such term. 𝔼 now gets stuck on the symbol the way it gets stuck on
# a λ name no entry of the '--symbolic' file answers, so '--partial' parks the
# site: 'a' is left exactly as it was written, a taint with no root. The site
# is written to the protocol as 'unanswered(𝜎1)', spelled the way every term
# carrying that symbol spells it.
symbolic: '[]'
location: 'Q.a'
partial: true
input: '⟦ a ↦ ⟦ λ ⤍ 𝜎1 ⟧.plus( 5 ) ⟧'
result: '𝜎1:λ.plus( 5 )'
protocol: |
  𝕄(Φ.a):
    unanswered(𝜎1)  # 𝕄(𝜎1:λ)