DeBruijn.Internal.Lvl

de Bruijn levels for well-scoped terms.

Levels

newtype Lvl ctx

de Bruijn levels.

Constructors

UnsafeLvl Int

Instances

Sinkable Lvl

Defined in DeBruijn.Internal.Lvl

Methods

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

Show (Lvl ctx)

Defined in DeBruijn.Internal.Lvl

Methods

showsPrec :: Int -> Lvl ctx -> ShowS

show :: Lvl ctx -> String

showList :: [Lvl ctx] -> ShowS

Eq (Lvl ctx)

Defined in DeBruijn.Internal.Lvl

Methods

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

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

Ord (Lvl ctx)

Defined in DeBruijn.Internal.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

idxToLvl :: Size ctx -> Idx ctx -> Lvl ctx

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

Last level.

>>> lvlZ S1
1

>>> lvlZ S5
5

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

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.

Methods

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

Instances

Sinkable Lvl

Defined in DeBruijn.Internal.Lvl

Methods

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

Sinkable (Proxy :: Ctx -> Type)

Defined in DeBruijn.Internal.Lvl

Methods

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

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

Sink term.

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

Essentially fmap sink

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

Sink term from empty context to a context of given size.

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

Essentially fmap . sinkSize

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')