Fcf.Data.Nat

Natural numbers.

Note that the operators from this module conflict with GHC.TypeLits and GHC.TypeNats.

Reexported type

From GHC.TypeNats.

data Nat

(Kind) This is the kind of type-level natural numbers.

Instances

type Eval (a ^ b :: Nat -> Type)

Defined in Fcf.Data.Nat

type Eval (a ^ b :: Nat -> Type) = a ^ b

type Eval (a * b :: Nat -> Type)

Defined in Fcf.Data.Nat

type Eval (a * b :: Nat -> Type) = a * b

type Eval (a - b :: Nat -> Type)

Defined in Fcf.Data.Nat

type Eval (a - b :: Nat -> Type) = a - b

type Eval (a + b :: Nat -> Type)

Defined in Fcf.Data.Nat

type Eval (a + b :: Nat -> Type) = a + b

type Eval (Sum ns :: Nat -> Type)

Defined in Fcf.Class.Foldable

type Eval (Sum ns :: Nat -> Type) = Eval (Foldr (+) 0 ns)

type Eval (Length (a2 ': as) :: Nat -> Type)

Defined in Fcf.Data.List

type Eval (Length (a2 ': as) :: Nat -> Type) = 1 + Eval (Length as)

type Eval (Length ('[] :: [a]) :: Nat -> Type)

Defined in Fcf.Data.List

type Eval (Length ('[] :: [a]) :: Nat -> Type) = 0

type Eval (Compare a b :: Ordering -> Type)

Defined in Fcf.Class.Ord

type Eval (Compare a b :: Ordering -> Type) = CmpNat a b

type Eval (FindIndex p (a2 ': as) :: Maybe Nat -> Type)

Defined in Fcf.Data.List

type Eval (FindIndex p (a2 ': as) :: Maybe Nat -> Type) = Eval (If (Eval (p a2)) (Pure ('Just 0)) ((Map ((+) 1) :: Maybe Nat -> Maybe Nat -> Type) =<< FindIndex p as))

type Eval (FindIndex _p ('[] :: [a]) :: Maybe Nat -> Type)

Defined in Fcf.Data.List

type Eval (FindIndex _p ('[] :: [a]) :: Maybe Nat -> Type) = 'Nothing :: Maybe Nat

Operations

data (+) :: Nat -> Nat -> Exp Nat

Instances

type Eval (a + b :: Nat -> Type)

Defined in Fcf.Data.Nat

type Eval (a + b :: Nat -> Type) = a + b

data (-) :: Nat -> Nat -> Exp Nat

Instances

type Eval (a - b :: Nat -> Type)

Defined in Fcf.Data.Nat

type Eval (a - b :: Nat -> Type) = a - b

data * :: Nat -> Nat -> Exp Nat

Instances

type Eval (a * b :: Nat -> Type)

Defined in Fcf.Data.Nat

type Eval (a * b :: Nat -> Type) = a * b

data (^) :: Nat -> Nat -> Exp Nat

Instances

type Eval (a ^ b :: Nat -> Type)

Defined in Fcf.Data.Nat

type Eval (a ^ b :: Nat -> Type) = a ^ b

Comparisons

Note that these conflict with Fcf.Class.Ord.

data (<=) :: Nat -> Nat -> Exp Bool

Instances

type Eval (a <= b :: Bool -> Type)

Defined in Fcf.Data.Nat

type Eval (a <= b :: Bool -> Type) = a <=? b

data (>=) :: Nat -> Nat -> Exp Bool

Instances

type Eval (a >= b :: Bool -> Type)

Defined in Fcf.Data.Nat

type Eval (a >= b :: Bool -> Type) = b <=? a

data (<) :: Nat -> Nat -> Exp Bool

Instances

type Eval (a < b :: Bool -> Type)

Defined in Fcf.Data.Nat

type Eval (a < b :: Bool -> Type) = Eval (Not =<< (a >= b))

data (>) :: Nat -> Nat -> Exp Bool

Instances

type Eval (a > b :: Bool -> Type)

Defined in Fcf.Data.Nat

type Eval (a > b :: Bool -> Type) = Eval (Not =<< (a <= b))