Nuprl Definition : eclass-state
eclass-state(init;f;X) ==  loop-class((λi,a,b. {f i a b} o X);λl.{init l})
Definitions occuring in Statement : 
loop-class: loop-class(X;init)
, 
eclass1: (f o X)
, 
apply: f a
, 
lambda: λx.A[x]
, 
single-bag: {x}
FDL editor aliases : 
eclass-state
Latex:
eclass-state(init;f;X)  ==    loop-class((\mlambda{}i,a,b.  \{f  i  a  b\}  o  X);\mlambda{}l.\{init  l\})
Date html generated:
2015_07_21-PM-02_41_07
Last ObjectModification:
2012_08_15-AM-02_18_26
Home
Index