Safe Haskell | Safe-Inferred |
---|---|
Language | Haskell2010 |
Synopsis
- class KnownNat (n :: Nat)
- type (<=) (x :: k) (y :: k) = (x <=? y) ~ 'True
- type family (a :: Natural) + (b :: Natural) :: Natural where ...
- type family (a :: Natural) * (b :: Natural) :: Natural where ...
- type family (a :: Natural) ^ (b :: Natural) :: Natural where ...
- type family (a :: Natural) - (b :: Natural) :: Natural where ...
- type family CmpNat (a :: Natural) (b :: Natural) :: Ordering where ...
- type family Div (a :: Natural) (b :: Natural) :: Natural where ...
- type family Mod (a :: Natural) (b :: Natural) :: Natural where ...
- type family Log2 (a :: Natural) :: Natural where ...
- type Nat = Natural
- data NaturalType bn where
- MkNaturalType :: KnownNat bn => NaturalType bn
- zeroNaturalType :: NaturalType 0
- succNaturalType :: NaturalType a -> NaturalType (a + 1)
- addNaturalType :: NaturalType a -> NaturalType b -> NaturalType (a + b)
- multiplyNaturalType :: NaturalType a -> NaturalType b -> NaturalType (a * b)
- type family PeanoToNatural pn where ...
- peanoToNaturalType :: PeanoNatType pn -> NaturalType (PeanoToNatural pn)
Documentation
This class gives the integer associated with a type-level natural. There are instances of the class for every concrete literal: 0, 1, 2, etc.
Since: base-4.7.0.0
natSing
type (<=) (x :: k) (y :: k) = (x <=? y) ~ 'True infix 4 #
Comparison (<=) of comparable types, as a constraint.
Since: base-4.16.0.0
type family (a :: Natural) + (b :: Natural) :: Natural where ... infixl 6 #
Addition of type-level naturals.
Since: base-4.7.0.0
type family (a :: Natural) * (b :: Natural) :: Natural where ... infixl 7 #
Multiplication of type-level naturals.
Since: base-4.7.0.0
type family (a :: Natural) ^ (b :: Natural) :: Natural where ... infixr 8 #
Exponentiation of type-level naturals.
Since: base-4.7.0.0
type family (a :: Natural) - (b :: Natural) :: Natural where ... infixl 6 #
Subtraction of type-level naturals.
Since: base-4.7.0.0
type family CmpNat (a :: Natural) (b :: Natural) :: Ordering where ... #
Comparison of type-level naturals, as a function.
Since: base-4.7.0.0
type family Div (a :: Natural) (b :: Natural) :: Natural where ... infixl 7 #
Division (round down) of natural numbers.
Div x 0
is undefined (i.e., it cannot be reduced).
Since: base-4.11.0.0
type family Mod (a :: Natural) (b :: Natural) :: Natural where ... infixl 7 #
Modulus of natural numbers.
Mod x 0
is undefined (i.e., it cannot be reduced).
Since: base-4.11.0.0
type family Log2 (a :: Natural) :: Natural where ... #
Log base 2 (round down) of natural numbers.
Log 0
is undefined (i.e., it cannot be reduced).
Since: base-4.11.0.0
A type synonym for Natural
.
Prevously, this was an opaque data type, but it was changed to a type synonym.
Since: base-4.16.0.0
data NaturalType bn where Source #
MkNaturalType :: KnownNat bn => NaturalType bn |
Instances
succNaturalType :: NaturalType a -> NaturalType (a + 1) Source #
addNaturalType :: NaturalType a -> NaturalType b -> NaturalType (a + b) Source #
multiplyNaturalType :: NaturalType a -> NaturalType b -> NaturalType (a * b) Source #
type family PeanoToNatural pn where ... Source #
PeanoToNatural 'Zero = 0 | |
PeanoToNatural ('Succ pn) = PeanoToNatural pn + 1 |
peanoToNaturalType :: PeanoNatType pn -> NaturalType (PeanoToNatural pn) Source #