first-class-families-0.8.2.0: First-class type families

Safe Haskell | Safe-Inferred
Language | Haskell2010

Fcf.Data.Nat

Contents

- Reexported type
- Operations
- Comparisons

Description

Natural numbers.

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

Synopsis

- type Nat = Natural
- data ((a :: Nat) + (b :: Nat)) (c :: Nat)
- data ((a :: Nat) - (b :: Nat)) (c :: Nat)
- data ((a :: Nat) * (b :: Nat)) (c :: Nat)
- data ((a :: Nat) ^ (b :: Nat)) (c :: Nat)
- data ((a :: Nat) <= (b :: Nat)) (c :: Bool)
- data ((a :: Nat) >= (b :: Nat)) (c :: Bool)
- data ((a :: Nat) < (b :: Nat)) (c :: Bool)
- data ((a :: Nat) > (b :: Nat)) (c :: Bool)

# Reexported type

From GHC.TypeNats.

type Nat = Natural Source #

A type synonym for `Natural`.

Previously, this was an opaque data type, but it was changed to a type synonym.

Since: base-4.16.0.0

# Operations

data ((a :: Nat) + (b :: Nat)) (c :: Nat) Source #

#### Instances

Instances details

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

data ((a :: Nat) - (b :: Nat)) (c :: Nat) Source #

#### Instances

Instances details

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

data ((a :: Nat) * (b :: Nat)) (c :: Nat) Source #

#### Instances

Instances details

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

data ((a :: Nat) ^ (b :: Nat)) (c :: Nat) Source #

#### Instances

Instances details

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

# Comparisons

Note that these conflict with Fcf.Class.Ord.

data ((a :: Nat) <= (b :: Nat)) (c :: Bool) Source #

#### Instances

Instances details

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

data ((a :: Nat) >= (b :: Nat)) (c :: Bool) Source #

#### Instances

Instances details

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

data ((a :: Nat) < (b :: Nat)) (c :: Bool) Source #

#### Instances

Instances details

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

data ((a :: Nat) > (b :: Nat)) (c :: Bool) Source #

#### Instances

Instances details

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