Nuprl Definition : bag-remove1

bag-remove1(eq;bs;a) ==  bag_remove1_aux(eq;[];a;bs)


Definitions occuring in Statement :  bag_remove1_aux: bag_remove1_aux(eq;checked;a;as),  nil: []
Definitions occuring in definition :  bag_remove1_aux: bag_remove1_aux(eq;checked;a;as),  nil: []
FDL editor aliases :  bag-remove1
Latex:
bag-remove1(eq;bs;a)  ==    bag\_remove1\_aux(eq;[];a;bs)


Date html generated: 2016_05_15-PM-08_03_47
Last ObjectModification: 2015_09_23-AM-08_20_47

Theory : bags_2


Home Index