Safe Haskell	Safe
Language	Haskell2010

Fcf.Data.Nat

Contents

Description

Natural numbers.

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

Synopsis

Reexported type

data Nat #

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

Instances

type Eval (a ^ b :: Nat -> Type) Source #
Instance details Defined in Fcf.Data.Nat type Eval (a ^ b :: Nat -> Type) = a ^ b
type Eval (a * b :: Nat -> Type) Source #
Instance details Defined in Fcf.Data.Nat type Eval (a * b :: Nat -> Type) = a * b
type Eval (a - b :: Nat -> Type) Source #
Instance details Defined in Fcf.Data.Nat type Eval (a - b :: Nat -> Type) = a - b
type Eval (a + b :: Nat -> Type) Source #
Instance details Defined in Fcf.Data.Nat type Eval (a + b :: Nat -> Type) = a + b
type Eval (Length (a2 ': as) :: Nat -> Type) Source #
Instance details Defined in Fcf.Data.List type Eval (Length (a2 ': as) :: Nat -> Type) = 1 + Eval (Length as)
type Eval (Length ([] :: [a]) :: Nat -> Type) Source #
Instance details Defined in Fcf.Data.List type Eval (Length ([] :: [a]) :: Nat -> Type) = 0
type Eval (FindIndex p (a2 ': as) :: Maybe Nat -> Type) Source #
Instance details 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) Source #
Instance details Defined in Fcf.Data.List type Eval (FindIndex _p ([] :: [a]) :: Maybe Nat -> Type) = (Nothing :: Maybe Nat)

Operations

Instances

type Eval (a + b :: Nat -> Type) Source #
Instance details Defined in Fcf.Data.Nat type Eval (a + b :: Nat -> Type) = a + b

Instances

type Eval (a - b :: Nat -> Type) Source #
Instance details Defined in Fcf.Data.Nat type Eval (a - b :: Nat -> Type) = a - b

Instances

type Eval (a * b :: Nat -> Type) Source #
Instance details Defined in Fcf.Data.Nat type Eval (a * b :: Nat -> Type) = a * b

Instances

type Eval (a ^ b :: Nat -> Type) Source #
Instance details Defined in Fcf.Data.Nat type Eval (a ^ b :: Nat -> Type) = a ^ b

Instances

type Eval (a <= b :: Bool -> Type) Source #
Instance details Defined in Fcf.Data.Nat type Eval (a <= b :: Bool -> Type) = a <=? b

Instances

type Eval (a >= b :: Bool -> Type) Source #
Instance details Defined in Fcf.Data.Nat type Eval (a >= b :: Bool -> Type) = b <=? a

Instances

type Eval (a < b :: Bool -> Type) Source #
Instance details Defined in Fcf.Data.Nat type Eval (a < b :: Bool -> Type) = Eval (Not =<< (a >= b))

Instances

type Eval (a > b :: Bool -> Type) Source #
Instance details Defined in Fcf.Data.Nat type Eval (a > b :: Bool -> Type) = Eval (Not =<< (a <= b))