Nuprl Definition : l-union'
l-union'(eq; as; bs) == cbv_list_accum(L,x.if x ∈b L then L else [x / L] fi ;as;bs)
Definitions occuring in Statement :
cbv_list_accum: cbv_list_accum(x,a.f[x; a];y;L),
deq-member: x ∈b L,
cons: [a / b],
ifthenelse: if b then t else f fi
Definitions occuring in definition :
cbv_list_accum: cbv_list_accum(x,a.f[x; a];y;L),
ifthenelse: if b then t else f fi ,
deq-member: x ∈b L,
cons: [a / b]
Latex:
l-union'(eq; as; bs) == cbv\_list\_accum(L,x.if x \mmember{}\msubb{} L then L else [x / L] fi ;as;bs)
Date html generated:
2016_05_14-PM-03_24_28
Last ObjectModification:
2015_09_22-PM-05_59_40
Theory : decidable!equality
Home
Index