transitive encapsulation operator is not implemented

[yegor256]

This is my expression:

{⟦ foo ↦ ⟦ t ↦ ⟦ k ↦ ⟦ bar ↦ ∅ ⟧ ⟧ ⟧ ⟧}

This is what I want to do:

name: foo
pattern: '⟦ 𝜏 ↝ ∅ ⟧'    # pay attention, a new arrow symbol here!
result: '⟦ 𝜏 ↦ ⟦⟧ ⟧'

In order to get this:

{⟦ foo ↦ ⟦⟧ ⟧}

We introduced this "transitive encapsulation" operator in this paper. Simply put, 𝜏 ↝ ∅ means that 𝜏 is bound to ∅ through a number of formations.

[yegor256]

@maxonfjvipon FYI

[maxonfjvipon]

@yegor256 is it really necessary right now? Can we close it?

[yegor256]

@maxonfjvipon it's not urgent, but we definitely need this