Data.Sized.Peano

This module exports Sized type specialized to type-level Peano 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 Z => 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 => (~) Nat n Z => Sized f n a