phino-0.0.157: test-resources/evaluate-packs/binds-a-copy-over-no-bare-symbol-as-it-is.yaml

# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com
# SPDX-License-Identifier: MIT
---
# yamllint disable rule:line-length
# A 'defer' line defers only a copy one of whose arguments reads to a bare
# symbol (#1892, #1933). Here 'Φ.items.tail' reads to an object that knows
# its 'next', so the line binds the copy as it is and the answer carries the
# copy whole. No 'deferred' line is written and no symbol is minted for it.
symbolic: |
  - λ: L_hold
    morph:
      𝑛1: $.b
    defer:
      𝑛2: 𝑛1
    𝑛: ⟦ φ ↦ 𝑛2 ⟧
location: 'Q.y'
input: '⟦ step(tup) ↦ ⟦ φ ↦ tup.next ⟧, items ↦ ⟦ tail ↦ ⟦ next ↦ ⟦ φ ↦ ⟦ λ ⤍ 𝜎1 ⟧ ⟧ ⟧ ⟧, y ↦ ⟦ b ↦ Φ.step( tup ↦ Φ.items.tail ), λ ⤍ L_hold ⟧.φ ⟧'
result: '⟦ tup ↦ Φ.items.tail, φ ↦ tup.next ⟧'
protocol: |
  𝕄(Φ.y):
    𝔼(L_hold):
      𝕄(Φ.a🌵0):
        𝑛·1·1 := Φ.step( tup ↦ Φ.items.tail )
      𝑛1·1 := 𝑛·1·1  # 𝕄(ξ.b)
      𝑛2·1 := 𝑛·1·1  # 𝑛1
      𝑛·1·2 := 𝑛·1·1:φ  # 𝑛
      𝑛·1·3 := 𝑛·1·1:φ  # 𝕄(𝑛·1·2)