Safe Haskell	Trustworthy
Language	Haskell2010

DeBruijn.Size

Contents

Common sizes

Synopsis

data Size (ctx :: Ctx) where
- pattern SZ :: () => m ~ EmptyCtx => Size m
- pattern SS :: forall m n. () => m ~ S n => Size n -> Size m
unSS :: forall (ctx :: Ctx). Size (S ctx) -> Size ctx
sizeToInt :: forall (ctx :: Ctx). Size ctx -> Int
pattern S1 :: () => m ~ Ctx1 => Size m
pattern S2 :: () => m ~ Ctx2 => Size m
pattern S3 :: () => m ~ Ctx3 => Size m
pattern S4 :: () => m ~ Ctx4 => Size m
pattern S5 :: () => m ~ Ctx5 => Size m
pattern S6 :: () => m ~ Ctx6 => Size m
pattern S7 :: () => m ~ Ctx7 => Size m
pattern S8 :: () => m ~ Ctx8 => Size m
pattern S9 :: () => m ~ Ctx9 => Size m

Documentation

data Size (ctx :: Ctx) where Source #

Term level witness of the size of a context.

>>> SZ 0

>>> SS (SS SZ) 2

Bundled Patterns

pattern SZ :: () => m ~ EmptyCtx => Size m
pattern SS :: forall m n. () => m ~ S n => Size n -> Size m

Instances

Instances details

TestEquality Size Source #
Instance details Defined in DeBruijn.Internal.Size Methods testEquality :: forall (a :: Ctx) (b :: Ctx). Size a -> Size b -> Maybe (a :~: b) #
EqP Size Source #
Instance details Defined in DeBruijn.Internal.Size Methods eqp :: forall (a :: Ctx) (b :: Ctx). Size a -> Size b -> Bool #
GCompare Size Source #
Instance details Defined in DeBruijn.Internal.Size Methods gcompare :: forall (a :: Ctx) (b :: Ctx). Size a -> Size b -> GOrdering a b #
GEq Size Source #
Instance details Defined in DeBruijn.Internal.Size Methods geq :: forall (a :: Ctx) (b :: Ctx). Size a -> Size b -> Maybe (a :~: b) #
GShow Size Source #
Instance details Defined in DeBruijn.Internal.Size Methods gshowsPrec :: forall (a :: Ctx). Int -> Size a -> ShowS #
OrdP Size Source #
Instance details Defined in DeBruijn.Internal.Size Methods comparep :: forall (a :: Ctx) (b :: Ctx). Size a -> Size b -> Ordering #
Show (Size ctx) Source #
Instance details Defined in DeBruijn.Internal.Size Methods showsPrec :: Int -> Size ctx -> ShowS # show :: Size ctx -> String # showList :: [Size ctx] -> ShowS #
Eq (Size ctx) Source #
Instance details Defined in DeBruijn.Internal.Size Methods (==) :: Size ctx -> Size ctx -> Bool # (/=) :: Size ctx -> Size ctx -> Bool #
Ord (Size ctx) Source #
Instance details Defined in DeBruijn.Internal.Size Methods compare :: Size ctx -> Size ctx -> Ordering # (<) :: Size ctx -> Size ctx -> Bool # (<=) :: Size ctx -> Size ctx -> Bool # (>) :: Size ctx -> Size ctx -> Bool # (>=) :: Size ctx -> Size ctx -> Bool # max :: Size ctx -> Size ctx -> Size ctx # min :: Size ctx -> Size ctx -> Size ctx #

unSS :: forall (ctx :: Ctx). Size (S ctx) -> Size ctx Source #

Unapply SS. Occasionally more useful than pattern matching.

sizeToInt :: forall (ctx :: Ctx). Size ctx -> Int Source #

Convert Size to 'Int.

Common sizes

pattern S1 :: () => m ~ Ctx1 => Size m Source #

pattern S2 :: () => m ~ Ctx2 => Size m Source #

pattern S3 :: () => m ~ Ctx3 => Size m Source #

pattern S4 :: () => m ~ Ctx4 => Size m Source #

pattern S5 :: () => m ~ Ctx5 => Size m Source #

pattern S6 :: () => m ~ Ctx6 => Size m Source #

pattern S7 :: () => m ~ Ctx7 => Size m Source #

pattern S8 :: () => m ~ Ctx8 => Size m Source #

pattern S9 :: () => m ~ Ctx9 => Size m Source #