Nuprl Definition : list-accum
list-accum(t,a,h.f[t; a; h];b;L) ==
if L is a pair then let h,t = L
in list-accum(t,a,h.f[t; a; h];f[t; b; h];t) otherwise if L = Ax then b otherwise ⊥
Definitions occuring in Statement :
bottom: ⊥,
ispair: if z is a pair then a otherwise b,
isaxiom: if z = Ax then a otherwise b,
spread: spread def
Definitions occuring in definition :
ispair: if z is a pair then a otherwise b,
spread: spread def,
isaxiom: if z = Ax then a otherwise b,
bottom: ⊥
FDL editor aliases :
list-accum
Latex:
list-accum(t,a,h.f[t; a; h];b;L) ==
if L is a pair then let h,t = L
in list-accum(t,a,h.f[t; a; h];f[t; b; h];t)
otherwise if L = Ax then b otherwise \mbot{}
Date html generated:
2018_05_21-PM-00_18_52
Last ObjectModification:
2018_01_03-PM-01_22_36
Theory : list_0
Home
Index