heads-the-block-of-a-morph-operand-with-the-operand.yaml

# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com
# SPDX-License-Identifier: MIT
---
# yamllint disable rule:line-length
# An operand of 'morph' is reduced where it stands in the universe, under a
# name phino makes up for it, but the block the 𝕄 opens is headed by the
# operand as the entry spells it, the way the line binding its meta is
# commented, and not by that made-up name (#2145).
symbolic: |
  - λ: L_kept
    morph:
      𝑛1: $.x
    𝑛: ⟦ φ ↦ ⟦ λ ⤍ 𝜎 ⟧ ⟧
location: 'Q.y'
input: '⟦ bytes(φ) ↦ ⟦⟧, number(φ) ↦ ⟦ neg ↦ ⟦⟧ ⟧, y ↦ ⟦ x ↦ 5, λ ⤍ L_kept ⟧.φ ⟧'
result: '𝜎1:λ'
protocol: |
  𝕄(Φ.y):
    𝔼(L_kept):
      𝕄(ξ.x):
        𝑛·1·1 := 5.0
        morphed 𝑛·1·2 := 𝑛·1·1
      𝑛1·1 := 𝑛·1·2  # 𝕄(ξ.x)
      𝑛·1·3 := 𝜎1:λ:φ  # 𝑛
      𝕄(𝑛·1·3):
        morphed 𝑛·1·4 := 𝜎1:λ:φ
      𝑛·1·5 := 𝑛·1·4  # 𝕄(𝑛·1·3)
    morphed 𝑛·0·1 := 𝜎1:λ