Advent.Nat

Description

Synopsis

data Nat
- = Z
- | S Nat
type family FromNatural (n :: Natural) :: Nat where ...
class UnfoldNat (n :: Nat) where
- unfoldNat :: f 'Z -> (forall (m :: Nat). f m -> f ('S m)) -> f n

Documentation

Natural numbers (used for type index)

Constructors

Z	zero
S Nat	successor

type family FromNatural (n :: Natural) :: Nat where ... Source #

Covert from GHC type literal syntax to an inductively defined natural

Equations

FromNatural 0 = 'Z
FromNatural n = 'S (FromNatural (n - 1))

class UnfoldNat (n :: Nat) where Source #

Methods

unfoldNat :: f 'Z -> (forall (m :: Nat). f m -> f ('S m)) -> f n Source #

Instances details

UnfoldNat 'Z Source #
Instance details Defined in Advent.Nat Methods unfoldNat :: f 'Z -> (forall (m :: Nat). f m -> f ('S m)) -> f 'Z Source #
UnfoldNat n => UnfoldNat ('S n) Source #
Instance details Defined in Advent.Nat Methods unfoldNat :: f 'Z -> (forall (m :: Nat). f m -> f ('S m)) -> f ('S n) Source #