parks-a-firing-whose-operand-never-came-down.yaml

# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com
# SPDX-License-Identifier: MIT
---
# The operand of a firing is itself stuck on a λ function no entry answers, so
# under '_partial' the block of the firing opens and binds nothing: 𝛿1 never
# came down, and the whole term is handed back the way it was reached.
symbolic: |
  - λ: L_pair
    dataize:
      𝛿1: $.x
    𝑛: ⟦ λ ⤍ 𝜎 ⟧
location: 'Q.y'
partial: true
input: >
  ⟦ y ↦ ⟦ x ↦ ⟦ λ ⤍ L_none ⟧.foo,
          λ ⤍ L_pair ⟧.z ⟧
result: '⟦ x ↦ L_none:λ.foo, λ ⤍ L_pair ⟧.z'
protocol: |
  𝕄(Φ.y):
    𝔼(L_pair):
      𝔻(Φ.a🌵0):
        𝕄(Φ.a🌵0):
          unanswered(L_none)  # 𝕄(L_none:λ)
      stuck(L_none)