remints-a-decorator-as-the-symbol-its-phi-comes-to.yaml

# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com
# SPDX-License-Identifier: MIT
---
# yamllint disable rule:line-length
# Morphing stops at a formation, so the tail of the pair below, a call of
# 'as-number' the way EO's 'length.plus( 1 ).as-number' is one, comes to the
# object 'as-number' and not to the number it decorates. A 'remint' step then
# morphs the φ of what the term came to, once per decorator, until a φ chain
# ends in the bare symbol '𝜎2', and answers that symbol (#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: '⟦ number(φ) ↦ ⟦⟧, bytes(φ) ↦ ⟦ as-number ↦ ⟦ ρ ↦ ∅, φ ↦ Φ.number( φ ↦ ξ.ρ ) ⟧ ⟧, y ↦ ⟦ x ↦ ⟦ head ↦ ⟦ λ ⤍ 𝜎1 ⟧, tail ↦ Φ.bytes( φ ↦ ⟦ λ ⤍ 𝜎2 ⟧ ).as-number ⟧, λ ⤍ L_shrink ⟧.tail ⟧'
result: '𝜎2:λ'
protocol: |
  𝕄(Φ.y):
    𝔼(L_shrink):
      𝑛1·1 := ⟦ head ↦ 𝜎1:λ, tail ↦ Φ.bytes( φ ↦ 𝜎2:λ ).as-number ⟧  # 𝕄(ξ.x)
      𝕄(Φ.bytes( φ ↦ 𝜎2:λ ).as-number):
        𝑛·1·1 := Φ.bytes( φ ↦ 𝜎2:λ )
      𝕄(𝑛·1·1.as-number.φ):
        𝑛·1·2 := Φ.number( φ ↦ 𝑛·1·1 )
      𝕄(𝑛·1·1.as-number.φ.φ):
        𝑛·1·3 := Φ.bytes( φ ↦ 𝜎2:λ )
      𝑛2·1 := ⟦ head ↦ 𝜎1:λ, tail ↦ 𝜎2:λ ⟧  # 𝑛1
      𝑛·1·4 := ⟦ head ↦ 𝜎1:λ, tail ↦ 𝜎2:λ ⟧  # 𝑛
      𝑛·1·5 := ⟦ head ↦ 𝜎1:λ, tail ↦ 𝜎2:λ ⟧  # 𝕄(𝑛·1·4)