Nuprl Definition : State-loc-comb
State-loc-comb(init;f;X) == λl,x,s. if bag-null(x) then s else lifting-loc-2(f) l x s fi |Loc, X, Prior(self)?init|
Definitions occuring in Statement :
lifting-loc-2: lifting-loc-2(f),
rec-combined-loc-class-opt-1: F|Loc, X, Prior(self)?init|,
ifthenelse: if b then t else f fi ,
apply: f a,
lambda: λx.A[x],
bag-null: bag-null(bs)
FDL editor aliases :
State-loc-comb
Latex:
State-loc-comb(init;f;X) ==
\mlambda{}l,x,s. if bag-null(x) then s else lifting-loc-2(f) l x s fi |Loc, X, Prior(self)?init|
Date html generated:
2016_05_17-AM-10_00_37
Last ObjectModification:
2012_11_30-PM-04_56_29
Theory : classrel!lemmas
Home
Index