I have proposed a hand-made, ugly variant of subtraction code for the Peano-Church arithmetic with an explicit recursive function and equality. Christian Sievers put me into order, thanks. Christian Sievers: > Compared to using equality, I think the following is really better: > dec n = fst (n (\(_,b)->(b,inc b)) (zer,zer)) where zer s z = z > > Of course, you wouldn't really use built-in pairing, would you? > > Christian Sievers Of course, not. I have sinned already very badly, but as we, the True Fighters (I have used Fortran for 15 years...) want to go to Fully Functional Heaven, I would of course define cons a b s = s a b car cs = cs const cdr cs = cs (flip const) And this: dec n = car (n (\z->cons (cdr z) (inc (cdr z))) (cons zer zer)) is almost perfect, although the Bishop of my Church would lambdify the internal (cdr z) for the sake of sane efficiency. Jerzy Karczmarczuk
