`𝜏?` syntax would be helpful (for matching what's not used later)

[yegor256]

This is my rule:

name: foo
pattern: '⟦ 𝜏1 ↦ 𝑒1, 𝜏2 ↦ 𝑒2 ⟧'
result: '⟦ x ↦ "yes!" ⟧'

Here, none of the substitutions are used in the result. However, I need to invent names for them, like 𝜏1 and 𝜏2.

Would be more convenient to use 𝜏? (or 𝜏*), which means 𝜏 whatever. It's uniquely matched, but not used in the result.

Maybe, for the sake of brevity, we may agree that 𝜏 (without index) means 𝜏 whatever. If index is specified, it's a specific match, possibly used in the result.

[maxonfjvipon]

@yegor256 what about 𝜏' or !a'. Apostrophe is not used anywhere else so there's no syntax intersection. ? is used in void binding, * is used in tails

[yegor256]

@maxonfjvipon can we just do 𝜏 instead? If there is nothing after it, it's anonymous and can't be used in the result. This would be the most compact way, since it's the most often situation to meet. WDYT?

[maxonfjvipon]

@yegor256 our normalization rules will become look ugly, like this dot:

⟦𝐵1, 𝜏1 ↦ 𝑒1, 𝐵2⟧.𝜏1

Or miss:

⟦𝐵⟧(𝜏1 ↦ 𝑒)

[yegor256]

@maxonfjvipon doesn't look ugly to me. The part 𝜏1 ↦ 𝑒1 says explicitly: "𝜏1 attribute attached to 𝑒1, while both of them to be used later".

[maxonfjvipon]

@yegor256 maybe Rdot isn't ugly, but there are other rules which use only one 𝜏. Then we should introduce such mechanism for meta bindings and meta expressions. They should have index then. That's definitely would be less beautiful than it's now

[yegor256]

@maxonfjvipon indeed, this new syntax will make short normalization rules more verbose. But it will make larger optimization rules more readable. In the end, this is what matters more -- readability of larger rules.