phino-0.0.154: test-resources/evaluate-packs/parks-an-evaluate-line-over-a-branch-left-unreduced.yaml

# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com
# SPDX-License-Identifier: MIT
---
# yamllint disable rule:line-length
# Under '--partial' a branch that got stuck comes back as the term it was
# parked at, which is no formation and so nothing 𝔼 can be asked of: the
# 'evaluate' line gets stuck on the fork itself, and the site the fork
# stands at is parked (#1874).
symbolic: |
  - λ: L_fork
    morph:
      𝑛1: $.a
    evaluate:
      𝑛2: 𝑛1
    𝑛: 𝑛2
location: 'Q.y'
partial: true
input: '⟦ y ↦ ⟦ a ↦ ⟦ λ ⤍ L_none ⟧.x, λ ⤍ L_fork ⟧.φ ⟧'
result: '⟦ a ↦ ⟦ λ ⤍ L_none ⟧.x, λ ⤍ L_fork ⟧.φ'
protocol: |
  𝕄(Φ.y):
    𝔼(L_fork):
      𝕄(Φ.a🌵0):
        unanswered(L_none)  # 𝕄(L_none:λ)
      𝑛1·1 := L_none:λ.x  # 𝕄(ξ.a)
      stuck(L_fork)