random-tau-skips-program-wide.yaml

# SPDX-FileCopyrightText: Copyright (c) 2025 Objectionary.com
# SPDX-License-Identifier: MIT
---
# Demonstrates that random-tau steers clear of names taken anywhere in the
# document, not just in the formation being rewritten. The 'used' formation
# already owns 'a🌵0' and 'a🌵1', so the freshly minted label for 'target'
# must be 'a🌵2'.
input: |
  [[
    used -> [[ a🌵0 -> ⟦⟧, a🌵1 -> ⟦⟧ ]],
    target -> [[ x -> "foo" ]]
  ]]
output: |-
  [[
    used -> [[ a🌵0 -> ⟦⟧, a🌵1 -> ⟦⟧ ]],
    target -> [[ x -> "foo", a🌵2 -> ⟦⟧ ]]
  ]]
rules:
  custom:
    - name: append fresh tau into target
      pattern: |
        [[ x -> !e1 ]]
      result: |
        [[ x -> !e1, !t1 -> [[ ]] ]]
      where:
        - meta: '!t1'
          function: random-tau