Nuprl Definition : OnlyChanges

OnlyChanges(L) ==
  if L = Ax then L otherwise let h,t = L
                             in let a,s = h
                                in if s=0
                                   then OnlyChanges(t)
                                   else eval nz = NextNonZero(t) in

                                        if nz = Ax then [] otherwise eval ch = OnlyChanges(nz) in

                                                                     let h',t' = nz

                                                                     in let b,s' = h'

                                                                        in if s'=-s then [<a, b> / ch] else ch

Definitions occuring in Statement : NextNonZero: NextNonZero(L), cons: [a / b], nil: [], callbyvalue: callbyvalue, isaxiom: if z = Ax then a otherwise b, int_eq: if a=b then c else d, spread: spread def, pair: <a, b>, minus: -n, natural_number: $n
Definitions occuring in definition : natural_number: $n, NextNonZero: NextNonZero(L), isaxiom: if z = Ax then a otherwise b, nil: [], callbyvalue: callbyvalue, spread: spread def, int_eq: if a=b then c else d, minus: -n, cons: [a / b], pair: <a, b>
FDL editor aliases : OnlyChanges

Latex:
OnlyChanges(L) == if L = Ax then L otherwise let h,t = L in let a,s = h in if s=0 then OnlyChanges(t) else eval nz = NextNonZero(t) in if nz = Ax then [] otherwise eval ch = OnlyChanges(nz) in let h',t' = nz in let b,s' = h' in if s'=-s then [<a, b> / ch] else ch Date html generated: 2019_10_31-AM-06_22_18 Last ObjectModification: 2019_02_19-PM-01_38_14 Theory : reals_2 Home Index