DeBruijn.Size

Documentation

data Size ctx where

Term level witness of the size of the context.

>>> SZ
0

>>> SS (SS SZ)
2

Constructors

SZ :: Size EmptyCtx

SS :: !(Size ctx) -> Size (S ctx)

Instances

TestEquality Size

Defined in DeBruijn.Size

Methods

testEquality :: forall (a :: k) (b :: k). Size a -> Size b -> Maybe (a :~: b)

EqP Size

Defined in DeBruijn.Size

Methods

eqp :: forall (a :: k) (b :: k). Size a -> Size b -> Bool

GCompare Size

Defined in DeBruijn.Size

Methods

gcompare :: forall (a :: k) (b :: k). Size a -> Size b -> GOrdering a b

GEq Size

Defined in DeBruijn.Size

Methods

geq :: forall (a :: k) (b :: k). Size a -> Size b -> Maybe (a :~: b)

GShow Size

Defined in DeBruijn.Size

Methods

gshowsPrec :: forall (a :: k). Int -> Size a -> ShowS

OrdP Size

Defined in DeBruijn.Size

Methods

comparep :: forall (a :: k) (b :: k). Size a -> Size b -> Ordering

Show (Size ctx)

Defined in DeBruijn.Size

Methods

showsPrec :: Int -> Size ctx -> ShowS

show :: Size ctx -> String

showList :: [Size ctx] -> ShowS

Eq (Size ctx)

Defined in DeBruijn.Size

Methods

(==) :: Size ctx -> Size ctx -> Bool

(/=) :: Size ctx -> Size ctx -> Bool

Ord (Size ctx)

Defined in DeBruijn.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 :: Size (S ctx) -> Size ctx

sizeToInt :: 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