Nuprl Definition : class-pred
class-pred(X;es;e) == last(λe'.0 <z #(X es e')) e
Definitions occuring in Statement :
es-local-pred: last(P),
lt_int: i <z j,
apply: f a,
lambda: λx.A[x],
natural_number: $n,
bag-size: #(bs)
FDL editor aliases :
class-pred
Latex:
class-pred(X;es;e) == last(\mlambda{}e'.0 <z \#(X es e')) e
Date html generated:
2015_07_20-PM-03_57_35
Last ObjectModification:
2012_02_25-PM-01_59_20
Home
Index