Data.Sized.Builtin

This module exports Sized type specialized to GHC's built-in type 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 ~ 0 => 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, SingI n) => n ~ 0 => Sized f n a