data-debruijn-0.1.0.0: Fast and safe implementation of common compiler machinery.
Safe HaskellNone
LanguageGHC2021

Data.Type.Nat

Synopsis

Documentation

data Nat Source #

Type-level natural numbers.

Constructors

Z 
S Nat 

type family (n :: Nat) + (m :: Nat) :: Nat where ... Source #

Addition of type-level naturals.

Equations

'Z + m = m 
('S n) + m = 'S (n + m) 

type family Pred (n :: Nat) :: Nat where ... Source #

Predecessor of type-level naturals.

Equations

Pred ('S n) = n 

type Pos (n :: Nat) = n ~ 'S (Pred n) Source #

Pos n holds if n is non-zero.

type family (n :: Nat) <= (m :: Nat) :: Bool where ... Source #

Less-than-or-equal for type-level naturals.

Equations

'Z <= m = 'True 
('S n) <= 'Z = 'False 
('S n) <= ('S m) = n <= m