HORIZON HASKELLDocslts/ghc-9.10.xc74966e2026-09-27Search names, modules, packages, or :: a typeCtrl K

GHC 9.10.3 · lts/ghc-9.10.x · c74966e · 2026-09-27

Addition

2 declarations

Subtraction

1 declaration

Division

2 declarations
valuedivide :: Nat a -> Nat b -> Nat (Div a b)
#

Divide two numbers. Rounds down (towards zero)

Multiplication

1 declaration

Successor

2 declarations
valuesucc :: Nat a -> Nat (a + 1)
#

The successor of a number.

Compare

11 declarations

Constants

6 declarations
valuezero :: Nat 0
#

The number zero.

valueone :: Nat 1
#

The number one.

valuetwo :: Nat 2
#

The number two.

valueconstant :: KnownNat n => Nat n
#

Use GHC's built-in type-level arithmetic to create a witness of a type-level number. This only reduces if the number is a constant.

Unboxed Constants

2 declarations
valuezero# :: (# #) -> Nat# 0
#

The number zero. Unboxed.

valueone# :: (# #) -> Nat# 1
#

The number one. Unboxed.

Unboxed Pattern Synonyms

18 declarations

Convert

6 declarations
valuedemote :: Nat n -> Int
#

Extract the Int from a Nat. This is intended to be used at a boundary where a safe interface meets the unsafe primitives on top of which it is built.

valuewith :: Int -> (forall (n :: Nat). Nat n -> a) -> a
#

Run a computation on a witness of a type-level number. The argument Int must be greater than or equal to zero. This is not checked. Failure to upload this invariant will lead to a segfault.