Safe Haskell	Trustworthy
Language	Haskell2010

DeBruijn.Lvl

Contents

Synopsis

data Lvl ctx
lvlToIdx :: Size ctx -> Lvl ctx -> Idx ctx
lvlZ :: Size ctx -> Lvl (S ctx)
idxToLvl :: Size ctx -> Idx ctx -> Lvl ctx
class Sinkable t where
- mapLvl :: Lte ctx ctx' -> t ctx -> t ctx'
sink :: Sinkable t => t ctx -> t (S ctx)
sinkSize :: Sinkable t => Size ctx -> t EmptyCtx -> t ctx
sinkAdd :: Sinkable t => Add n ctx ctx' -> t ctx -> t ctx'
mapSink :: (Functor f, Sinkable t) => f (t ctx) -> f (t (S ctx))
mapSinkSize :: (Functor f, Sinkable t) => Size ctx -> f (t EmptyCtx) -> f (t ctx)
mapSinkAdd :: (Functor f, Sinkable t) => Add n ctx ctx' -> f (t ctx) -> f (t ctx')

Documentation

data Lvl ctx Source #

de Bruijn levels.

Instances details

Sinkable Lvl Source #
Instance details Defined in DeBruijn.Internal.Lvl Methods mapLvl :: forall (ctx :: Ctx) (ctx' :: Ctx). Lte ctx ctx' -> Lvl ctx -> Lvl ctx' Source #
Show (Lvl ctx) Source #
Instance details Defined in DeBruijn.Internal.Lvl Methods showsPrec :: Int -> Lvl ctx -> ShowS # show :: Lvl ctx -> String # showList :: [Lvl ctx] -> ShowS #
Eq (Lvl ctx) Source #
Instance details Defined in DeBruijn.Internal.Lvl Methods (==) :: Lvl ctx -> Lvl ctx -> Bool # (/=) :: Lvl ctx -> Lvl ctx -> Bool #
Ord (Lvl ctx) Source #
Instance details 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 Source #

Convert level to index.

>>> lvlToIdx S2 (lvlZ S1)
0

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

Last level.

>>> lvlZ S1
1

>>> lvlZ S5
5

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

Sinking

class Sinkable t where Source #

Sinkable terms can be weakened (sunk) cheaply.

Methods

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

Instances details

Sinkable Lvl Source #
Instance details Defined in DeBruijn.Internal.Lvl Methods mapLvl :: forall (ctx :: Ctx) (ctx' :: Ctx). Lte ctx ctx' -> Lvl ctx -> Lvl ctx' Source #
Sinkable (Proxy :: Ctx -> Type) Source #
Instance details Defined in DeBruijn.Internal.Lvl Methods mapLvl :: forall (ctx :: Ctx) (ctx' :: Ctx). Lte ctx ctx' -> Proxy ctx -> Proxy ctx' Source #

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

Sink term.

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

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

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

Essentially fmap sink

Essentially fmap . sinkSize

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