Rational arithmetic rebased

[hhefesto]

ready to fast forward

[sfultong]

my dream is to eventually be able to do something like this:

[Nat, toNat, nPlus, nMinus]
  = let wrapper = \h ->
                let N = \(hc, _) x -> assert (dEqual hc h) "not Natural"
                in [ N
                   , \x -> (h, x)
                   , \((_, aa) : N) ((_, bb) : N) -> (h, d2c aa succ bb)
                   , \((_, aa) : N) ((_, bb) : N) ->
                       let sLeft = \x -> case x of
                                              (l, _) -> l
                                              abort "can't subtract larger number from smaller one"
                       in (h, d2c bb sLeft aa)
                   ]
    in wrapper (# wrapper)

but that requires parser changes