representable-tries-1.8.0: Tries from representations of polynomial functors
Numeric.Nat.Zeroless
Description
Zeroless numbers encoded in zeroless binary numbers
data D0 Source
Constructors
0
Instances
data D1 n Source
2n + 1
data D2 n Source
2n + 2
type :+: n m = Add C0 n mSource
type family n :*: m Source
class Zeroless n whereSource
Methods
ind :: f D0 -> (forall m. Zeroless m => f m -> f (D1 m)) -> (forall m. Zeroless m => f m -> f (D2 m)) -> f nSource
caseNat :: forall r. (n ~ D0 => r) -> (forall x. (n ~ D1 x, Zeroless x) => x -> r) -> (forall x. (n ~ D2 x, Zeroless x) => x -> r) -> n -> rSource
type family Succ n Source
type family Pred n Source
type N1 = D1 D0Source
type N8 = D2 (D1 (D1 D0))Source
type N16 = D2 (D1 (D1 (D1 D0)))Source
type N32 = D2 (D1 (D1 (D1 (D1 D0))))Source
type N64 = D2 (D1 (D1 (D1 (D1 (D1 D0)))))Source
newtype Nat n Source
Fields
nat :: Zeroless n => Nat nSource
newtype Fin n Source
type Reverse n = Reverse' D0 nSource