walks-into-the-argument-of-an-atom-it-cannot-fire.yaml

# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com
# SPDX-License-Identifier: MIT
---
# Nothing demands the argument of a λ function that cannot fire, so 𝔻 never
# reaches it; the walk does, and the λ function around it stays in place.
location: 'Q.@'
model: true
symbolic: true
input: '[[ x -> [[ y -> ?, L> L_bar ]]( y -> 6.plus( 7 ) ) ]]'
result: |-
  ⟦ y ↦ ∅, λ ⤍ L_bar ⟧(
    y ↦ ⟦
      φ ↦ 𝜎1:λ,
      as-bytes ↦ φ,
      plus(ρ, x) ↦ L_number_plus:λ,
      times(ρ, x) ↦ L_number_times:λ,
      div(ρ, x) ↦ L_number_div:λ,
      gt(ρ, x) ↦ L_number_gt:λ,
      eq(ρ, x) ↦ ρ.as-bytes.eq( x.as-bytes ):φ,
      nope(ρ) ↦ L_number_nope:λ
    ⟧
  ):x