Nuprl Definition : face-or-list
\/(L) == reduce(λa,b. (a ∨ b);0(𝔽);L)
Definitions occuring in Statement :
face-or: (a ∨ b),
face-0: 0(𝔽),
reduce: reduce(f;k;as),
lambda: λx.A[x]
Definitions occuring in definition :
reduce: reduce(f;k;as),
lambda: λx.A[x],
face-or: (a ∨ b),
face-0: 0(𝔽)
FDL editor aliases :
face-or-list
Latex:
\mbackslash{}/(L) == reduce(\mlambda{}a,b. (a \mvee{} b);0(\mBbbF{});L)
Date html generated:
2016_05_19-AM-08_26_00
Last ObjectModification:
2016_03_05-PM-08_06_26
Theory : cubical!type!theory
Home
Index