CurryInfo: binint-3.0.0 / Data.BinInt.quotRemNat

quotRemNat :: Nat -> Nat -> (BinInt, BinInt)
quotRemNat x y
  | y == IHi  = (Pos x, Zero   ) -- quotRemNat x 1 = (x, 0)
  | x == IHi  = (Zero , Pos IHi) -- quotRemNat 1 y = (0, 1)
  | otherwise = case cmpNat x y of
      EQ -> (Pos IHi, Zero )   -- x = y : quotRemNat x y = (1, 0)
      LT -> (Zero   , Pos x)   -- x < y : quotRemNat x y = (0, x)
      GT -> case quotRemNat (div2 x) y of
        (Neg _, _    ) -> error "quotRemNat: negative quotient"
        (Zero , _    ) -> (Pos IHi  , x -^ y) -- x > y, x/2 < y  : quotRemNat x y = (1, x - y)
        (Pos _, Neg _) -> error "quotRemNat: negative remainder"
        (Pos d, Zero ) -> (Pos (O d), mod2 x)
        (Pos d, Pos m) -> case quotRemNat (shift x m) y of
          (Neg _ , _ ) -> error "quotRemNat: negative quotient"
          (Zero  , m') -> (Pos (O d)      , m')
          (Pos d', m') -> (Pos (O d +^ d'), m')
  where
    shift IHi   _ = error "quotRemNat.shift: IHi"
    shift (O _) n = O n
    shift (I _) n = I n

argument 2

deterministic operation

--- Quotient and remainder.

<FAILING>

referentially transparent operation

no fixity defined

{(_,_) |-> {(,)}}

quotRemNat

no precedence defined

{(,)}

Nat -> Nat -> (BinInt, BinInt)

operation might suspend on free variables

possibly non-terminating

possibly non-reducible on same data term