Nuprl Definition : mset_mon
mset_mon{s} == <MSet{s}, λx,y. eq_mset{s}(x,y), λx,y. tt, λx,y. (x + y), 0{s}, λx.x>
Definitions occuring in Statement :
eq_mset: eq_mset{s}(a,b),
mset_sum: a + b,
null_mset: 0{s},
mset: MSet{s},
btrue: tt,
lambda: λx.A[x],
pair: <a, b>
Definitions occuring in definition :
mset: MSet{s},
eq_mset: eq_mset{s}(a,b),
btrue: tt,
mset_sum: a + b,
pair: <a, b>,
null_mset: 0{s},
lambda: λx.A[x]
Latex:
mset\_mon\{s\} == <MSet\{s\}, \mlambda{}x,y. eq\_mset\{s\}(x,y), \mlambda{}x,y. tt, \mlambda{}x,y. (x + y), 0\{s\}, \mlambda{}x.x>
Date html generated:
2016_05_16-AM-07_47_02
Last ObjectModification:
2015_09_23-AM-09_52_03
Theory : mset
Home
Index