Data.Sized.Builtin

This module exports Sized type specialized to GHC's built-in type numeral Nat.

Documentation

type Ordinal n = Ordinal n

type Sized f n = Sized f n

module Data.Sized

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

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

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

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