Nuprl Definition : l_index
index(L;x) == mu(λi.(dT x L[i]))
Definitions occuring in Statement :
mu: mu(f),
select: L[n],
apply: f a,
lambda: λx.A[x]
Definitions occuring in definition :
mu: mu(f),
lambda: λx.A[x],
apply: f a,
select: L[n]
FDL editor aliases :
l_index
Latex:
index(L;x) == mu(\mlambda{}i.(dT x L[i]))
Date html generated:
2016_05_14-PM-03_31_50
Last ObjectModification:
2015_09_22-PM-06_00_50
Theory : decidable!equality
Home
Index