Nuprl Definition : bag-lex
bag-lex(n;f;g) ==
λas,bs. primrec(n;0;λm,v. if v=0 then eval i = (#g m in as) in eval j = (#g m in bs) in i - j else v)
Definitions occuring in Statement :
bag-count: (#x in bs),
primrec: primrec(n;b;c),
callbyvalue: callbyvalue,
eq_int: (i =z j),
int_eq: if a=b then c else d,
apply: f a,
lambda: λx.A[x],
subtract: n - m,
natural_number: $n
Definitions occuring in definition :
primrec: primrec(n;b;c),
int_eq: if a=b then c else d,
natural_number: $n,
callbyvalue: callbyvalue,
bag-count: (#x in bs),
lambda: λx.A[x],
eq_int: (i =z j),
apply: f a,
subtract: n - m
FDL editor aliases :
bag-lex
Latex:
bag-lex(n;f;g) ==
\mlambda{}as,bs. primrec(n;0;\mlambda{}m,v. if v=0
then eval i = (\#g m in as) in
eval j = (\#g m in bs) in
i - j
else v)
Date html generated:
2016_05_15-PM-08_13_32
Last ObjectModification:
2015_09_23-AM-08_21_07
Theory : bags_2
Home
Index