| Description: A nilad abstraction. When
used where a variable would normally belong, the variable used is instead the
first one written by 𝜑 to x. (Any other operations on x will block indefinitely, as they would on a fresh
channel.) This is a very useful concept, since this allows us to reason about
expressions which carry values.
Keep in mind that these must be treated linearly like everything else, so using
nilad variables multiple times may carry unintended consequences. Use ≔ as necessary to avoid this.
The nilad abstraction is characterized by df-nab 267. |