DeBruijn.Lvl

Documentation

data Lvl ctx

de Bruijn levels.

Instances

Sinkable Lvl

Defined in DeBruijn.Lvl

Methods

mapLvl :: forall (ctx :: Ctx) (ctx' :: Ctx). Lte ctx ctx' -> Lvl ctx -> Lvl ctx'

Show (Lvl ctx)

Defined in DeBruijn.Lvl

Methods

showsPrec :: Int -> Lvl ctx -> ShowS

show :: Lvl ctx -> String

showList :: [Lvl ctx] -> ShowS

Eq (Lvl ctx)

Defined in DeBruijn.Lvl

Methods

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

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

Ord (Lvl ctx)

Defined in DeBruijn.Lvl

Methods

compare :: Lvl ctx -> Lvl ctx -> Ordering

(<) :: Lvl ctx -> Lvl ctx -> Bool

(<=) :: Lvl ctx -> Lvl ctx -> Bool

(>) :: Lvl ctx -> Lvl ctx -> Bool

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

max :: Lvl ctx -> Lvl ctx -> Lvl ctx

min :: Lvl ctx -> Lvl ctx -> Lvl ctx

lvlToIdx :: Size ctx -> Lvl ctx -> Idx ctx

Convert level to index.

>>> lvlToIdx S2 (lvlZ S1)
0

lvlZ :: Size ctx -> Lvl (S ctx)

Last level.

>>> lvlZ S1
1

>>> lvlZ S5
5

sinkLvl :: Lvl ctx -> Lvl (S ctx)

Sink Lvl into a larger context.

>>> sinkLvl (lvlZ S3)
3

>>> sink (lvlZ S3)
3

>>> mapLvl (LS LZ) (lvlZ S3)
3

class Sinkable t where

Sinkable terms can be weakened (sunk) cheaply. (when Lvl is implemented as newtype over Int).

Methods

mapLvl :: Lte ctx ctx' -> t ctx -> t ctx'

Instances

Sinkable Lvl

Defined in DeBruijn.Lvl

Methods

mapLvl :: forall (ctx :: Ctx) (ctx' :: Ctx). Lte ctx ctx' -> Lvl ctx -> Lvl ctx'

sink :: Sinkable t => t ctx -> t (S ctx)

mapSink :: (Functor f, Sinkable t) => f (t ctx) -> f (t (S ctx))

sinkSize :: Sinkable t => Size ctx -> t EmptyCtx -> t ctx

mapSinkSize :: (Functor f, Sinkable t) => Size ctx -> f (t EmptyCtx) -> f (t ctx)

sinkAdd :: Sinkable t => Add n ctx ctx' -> t ctx -> t ctx'

mapSinkAdd :: (Functor f, Sinkable t) => Add n ctx ctx' -> f (t ctx) -> f (t ctx')