phino-0.0.156: test-resources/evaluate-packs/remints-a-term-as-the-symbol-its-phi-chain-ends-in.yaml

# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com
# SPDX-License-Identifier: MIT
---
# yamllint disable rule:line-length
# A rule of a 'rewrite' block may not write a 𝜎 into its result, but a 'where'
# step may call 'remint', which answers the symbol the term it is given stands
# for. A term whose φ chain ends in a bare symbol is that symbol, so nothing is
# minted and no line is written: the head of the pair below is '𝜎1' and its
# tail '𝜎2', whatever else the tail holds (#1923).
symbolic: |
  - λ: L_shrink
    morph:
      𝑛1: $.x
    rewrite:
      𝑛2:
        of: 𝑛1
        rules:
          - name: small-pair
            pattern: ⟦ !B1, head ↦ 𝑒1, tail ↦ 𝑒2, !B2 ⟧
            result: ⟦ !B1, head ↦ 𝑒3, tail ↦ 𝑒4, !B2 ⟧
            where:
              - meta: 𝑒3
                function: remint
                args: [𝑒1]
              - meta: 𝑒4
                function: remint
                args: [𝑒2]
    𝑛: 𝑛2
location: 'Q.y'
input: '⟦ y ↦ ⟦ x ↦ ⟦ head ↦ ⟦ φ ↦ ⟦ λ ⤍ 𝜎1 ⟧ ⟧, tail ↦ ⟦ φ ↦ ⟦ λ ⤍ 𝜎2 ⟧, k ↦ ⟦ λ ⤍ 𝜎3 ⟧ ⟧ ⟧, λ ⤍ L_shrink ⟧.tail ⟧'
result: '𝜎2:λ'
protocol: |
  𝕄(Φ.y):
    𝔼(L_shrink):
      𝑛1·1 := ⟦ head ↦ 𝜎1:λ:φ, tail ↦ ⟦ φ ↦ 𝜎2:λ, k ↦ 𝜎3:λ ⟧ ⟧  # 𝕄(ξ.x)
      𝑛2·1 := ⟦ head ↦ 𝜎1:λ, tail ↦ 𝜎2:λ ⟧  # 𝑛1
      𝑛·1·1 := ⟦ head ↦ 𝜎1:λ, tail ↦ 𝜎2:λ ⟧  # 𝑛
      𝑛·1·2 := ⟦ head ↦ 𝜎1:λ, tail ↦ 𝜎2:λ ⟧  # 𝕄(𝑛·1·1)