Nuprl Definition : dset_list
s List == mk_dset(|s| List, λx,y. (x =b y))
Definitions occuring in Statement :
eq_list: as =b bs,
list: T List,
lambda: λx.A[x],
mk_dset: mk_dset(T, eq),
set_car: |p|
Definitions occuring in definition :
mk_dset: mk_dset(T, eq),
list: T List,
set_car: |p|,
lambda: λx.A[x],
eq_list: as =b bs
Latex:
s List == mk\_dset(|s| List, \mlambda{}x,y. (x =\msubb{} y))
Date html generated:
2016_05_16-AM-07_34_54
Last ObjectModification:
2015_09_23-AM-09_51_28
Theory : list_2
Home
Index