Data.Sized.Peano

This module exports Sized type specialized to type-level Peano numeral Nat.

Documentation

type Ordinal (n :: Nat) = Ordinal n

type Sized f (n :: Nat) = Sized f n

module Data.Sized

pattern (:<) :: forall f (n :: Nat) a. ListLike (f a) a => forall (n1 :: Nat). (n ~ Succ n1, SingI n1) => a -> Sized f n1 a -> Sized f n a infixr 5

pattern NilL :: forall f (n :: Nat) a. ListLike (f a) a => n ~ Z => Sized f n a

pattern (:>) :: forall f (n :: Nat) a. ListLike (f a) a => forall (n1 :: Nat). (n ~ Succ n1, SingI n1) => Sized f n1 a -> a -> Sized f n a infixl 5

pattern NilR :: forall f (n :: Nat) a. ListLike (f a) a => n ~ Z => Sized f n a