Nuprl Definition : union-list2
union-list2(eq;ll) == rec-case(ll) of [] => [] | l1::l2 => r.if null(l2) then l1 else r ⋃ l1 fi
Definitions occuring in Statement :
l-union: as ⋃ bs,
null: null(as),
list_ind: list_ind,
nil: [],
ifthenelse: if b then t else f fi
Definitions occuring in definition :
list_ind: list_ind,
nil: [],
ifthenelse: if b then t else f fi ,
null: null(as),
l-union: as ⋃ bs
FDL editor aliases :
union-list2
Latex:
union-list2(eq;ll) == rec-case(ll) of [] => [] | l1::l2 => r.if null(l2) then l1 else r \mcup{} l1 fi
Date html generated:
2016_05_14-PM-03_25_22
Last ObjectModification:
2015_09_22-PM-05_59_42
Theory : decidable!equality
Home
Index