Nuprl Definition : in-missing
in-missing(i;missing) == reduce(λx,r. (x ≤z i ∧b ((x =z i) ∨br));ff;missing)
Definitions occuring in Statement :
reduce: reduce(f;k;as),
le_int: i ≤z j,
bor: p ∨bq,
band: p ∧b q,
eq_int: (i =z j),
bfalse: ff,
lambda: λx.A[x]
FDL editor aliases :
in-missing
Latex:
in-missing(i;missing) == reduce(\mlambda{}x,r. (x \mleq{}z i \mwedge{}\msubb{} ((x =\msubz{} i) \mvee{}\msubb{}r));ff;missing)
Date html generated:
2016_05_17-PM-01_44_39
Last ObjectModification:
2013_03_19-PM-01_48_51
Theory : datatype-signatures
Home
Index