Stability	experimental
Maintainer	ekmett@gmail.com

Numeric.Nat.Zeroless

Description

Zeroless numbers encoded in zeroless binary numbers

Documentation

data D0 Source

Constructors

D0

0

Instances

Zeroless D0

data D1 n Source

Constructors

D1 n

2n + 1

Instances

Zeroless n => Positive (D1 n)
Zeroless n => Zeroless (D1 n)

data D2 n Source

Constructors

D2 n

2n + 2

Instances

Zeroless n => Positive (D2 n)
Zeroless n => Zeroless (D2 n)

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

Instances

Zeroless D0
Zeroless n => Zeroless (D2 n)
Zeroless n => Zeroless (D1 n)

type family Succ n Source

type family Pred n Source

type N1 = D1 D0 Source

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

Constructors

Nat
Fields fromNat :: Int

Instances

Zeroless n => Bounded (Nat n)
Zeroless n => Enum (Nat n)
Zeroless n => Eq (Nat n)
Zeroless n => Ord (Nat n)
Zeroless n => Show (Nat n)

nat :: Zeroless n => Nat nSource

newtype Fin n Source

Constructors

Fin
Fields fromFin :: Int

Instances

Positive n => Bounded (Fin n)
Positive n => Enum (Fin n)
Eq (Fin n)
Positive n => Num (Fin n)
Ord (Fin n)
Show (Fin n)

type Reverse n = Reverse' D0 nSource