Nuprl Definition : NextNonZero
NextNonZero(L) == if L = Ax then L otherwise let h,t = L in if snd(h)=0 then NextNonZero(t) else L
Definitions occuring in Statement :
pi2: snd(t),
isaxiom: if z = Ax then a otherwise b,
int_eq: if a=b then c else d,
spread: spread def,
natural_number: $n
Definitions occuring in definition :
isaxiom: if z = Ax then a otherwise b,
spread: spread def,
int_eq: if a=b then c else d,
pi2: snd(t),
natural_number: $n
FDL editor aliases :
NextNonZero
Latex:
NextNonZero(L) == if L = Ax then L otherwise let h,t = L in if snd(h)=0 then NextNonZero(t) else L
Date html generated:
2019_10_31-AM-06_22_00
Last ObjectModification:
2019_02_19-PM-00_18_40
Theory : reals_2
Home
Index