phino-0.0.152: test-resources/evaluate-packs/joins-a-branch-with-a-decorator-of-it-when-lenient.yaml

# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com
# SPDX-License-Identifier: MIT
---
# yamllint disable rule:line-length
# A fork whose one branch calls a method often meets a decorator: one branch
# comes to a copy, the other to a formation whose φ is that copy. The two
# differ in shape, so a strict join refuses them. An entry that says
# 'lenient: true' joins them into the decorator, with a fresh symbol minted
# inside it the usual way (#1815).
symbolic: |
  - λ: L_fork
    morph:
      𝑛1: $.a
      𝑛2: $.b
    join:
      𝑛3: [𝑛1, 𝑛2]
    lenient: true
    𝑛: 𝑛3
location: 'Q.y'
input: '⟦ y ↦ ⟦ a ↦ ⟦ φ ↦ ⟦ λ ⤍ 𝜎1 ⟧, neg ↦ ⟦⟧ ⟧, b ↦ ⟦ φ ↦ ⟦ φ ↦ ⟦ λ ⤍ 𝜎2 ⟧, neg ↦ ⟦⟧ ⟧ ⟧, λ ⤍ L_fork ⟧.φ ⟧'
result: '⟦ φ ↦ 𝜎3:λ, neg ↦ ⟦⟧ ⟧'
protocol: |
  𝕄(Φ.y):
    𝔼(L_fork):
      𝑛1·1 := ⟦ φ ↦ 𝜎1:λ, neg ↦ ⟦⟧ ⟧  # 𝕄(ξ.a)
      𝑛2·1 := ⟦ φ ↦ 𝜎2:λ, neg ↦ ⟦⟧ ⟧:φ  # 𝕄(ξ.b)
      𝔻(𝜎3:λ) ∈ { 𝔻(𝜎1:λ), 𝔻(𝜎2:λ) }
      𝑛3·1 := ⟦ φ ↦ 𝜎3:λ, neg ↦ ⟦⟧ ⟧:φ  # [𝑛1, 𝑛2]
      𝑛·1·1 := 𝑛3·1  # 𝑛
      𝑛·1·2 := 𝑛3·1  # 𝕄(𝑛·1·1)