nvnab - Linear Logic Proof Explorer

	Linear Logic Proof Explorer	< Previous Next > Nearby theorems
Mirrors > Home > LLPE Home > Th. List > nvnab		Structured version

Syntax Definition nvnab 271

Description: A simple nilad abstraction. Ordinary nilad abstractions use the bound channel as a sort of return channel, while this version immediately returns a fresh channel.

**Hypotheses**
Ref	Expression
wph	wff 𝜑
vx	var x

**Assertion**
Ref	Expression
nvnab	nilad {νx \| 𝜑}

See definition df-vnab 272 for more information.

Colors of variables: wff var nilad

W3C validator