phino-0.0.152: test-resources/evaluate-packs/walks-on-past-a-binding-it-parked-on.yaml

# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com
# SPDX-License-Identifier: MIT
---
# A deep walk under '_partial': the binding stuck on a λ function no entry
# answers is left as it is, and the walk goes on to the binding after it
# instead of giving the whole run up.
symbolic: |
  - λ: L_answers
    𝑛: ⟦ foo ↦ ⟦⟧, λ ⤍ 𝜎 ⟧
location: 'Q'
deep: true
partial: true
input: >
  ⟦ x ↦ ⟦ λ ⤍ L_none, ρ ↦ ∅ ⟧.foo,
    y ↦ ⟦ λ ⤍ L_answers, ρ ↦ ∅ ⟧.foo ⟧
result: '⟦ x ↦ L_none:λ.foo, y ↦ L_answers:λ.foo ⟧'
protocol: |
  𝕄(Φ):
    𝕄(Φ.x):
      unanswered(L_none)  # 𝕄(L_none:λ)
    𝕄(Φ.y):
      𝔼(L_answers):
        𝑛·1·1 := ⟦ foo ↦ ⟦⟧, λ ⤍ 𝜎1 ⟧  # 𝑛
        𝑛·1·2 := ⟦ foo ↦ ⟦⟧, λ ⤍ 𝜎1 ⟧  # 𝕄(𝑛·1·1)