debruijn-safe-0.1: de Bruijn indices and levels
Safe HaskellSafe
LanguageHaskell2010

DeBruijn.Idx

Description

de Bruijn indices for well-scoped terms.

Synopsis

de Bruijn indices

data Idx n where Source #

de Bruijn indices.

>>> IS (IS (IS IZ))
3

Constructors

IZ :: Idx (S n) 
IS :: !(Idx n) -> Idx (S n) 

Instances

Instances details
Renamable Idx Source # 
Instance details

Defined in DeBruijn.Ren

Methods

rename :: forall (n :: Ctx) (m :: Ctx). Ren n m -> Idx n -> Idx m Source #

weaken :: forall (n :: Ctx) (m :: Ctx). Wk n m -> Idx n -> Idx m Source #

RenamableA Idx Source # 
Instance details

Defined in DeBruijn.Ren

Methods

renameA :: forall f (ctx :: Ctx) (ctx' :: Ctx). Applicative f => RenA f ctx ctx' -> Idx ctx -> f (Idx ctx') Source #

grename :: forall m f (ctx :: Ctx) (ctx' :: Ctx). IdxMapping f m => m ctx ctx' -> Idx ctx -> f (Idx ctx') Source #

Subst Idx Source # 
Instance details

Defined in DeBruijn.Sub

Methods

subst :: forall (ctx :: Ctx) (ctx' :: Ctx). Sub Idx ctx ctx' -> Idx ctx -> Idx ctx' Source #

Var Idx Source # 
Instance details

Defined in DeBruijn.Sub

Methods

var :: forall (ctx :: Ctx). Idx ctx -> Idx ctx Source #

Show (Idx j) Source # 
Instance details

Defined in DeBruijn.Idx

Methods

showsPrec :: Int -> Idx j -> ShowS #

show :: Idx j -> String #

showList :: [Idx j] -> ShowS #

Eq (Idx n) Source # 
Instance details

Defined in DeBruijn.Idx

Methods

(==) :: Idx n -> Idx n -> Bool #

(/=) :: Idx n -> Idx n -> Bool #

Ord (Idx n) Source # 
Instance details

Defined in DeBruijn.Idx

Methods

compare :: Idx n -> Idx n -> Ordering #

(<) :: Idx n -> Idx n -> Bool #

(<=) :: Idx n -> Idx n -> Bool #

(>) :: Idx n -> Idx n -> Bool #

(>=) :: Idx n -> Idx n -> Bool #

max :: Idx n -> Idx n -> Idx n #

min :: Idx n -> Idx n -> Idx n #

absurdIdx :: Idx EmptyCtx -> a Source #

Derive anything from index into empty scope.

Note: don't use EmptyCase as it doesn't work for unsafe representation.

unIdx :: a -> (Idx n -> a) -> Idx (S n) -> a Source #

Case on Idx. (compare to maybe).

idxToInt :: Idx n -> Int Source #

Convert index to Int.

Common indices

pattern I1 :: () => m ~ S (S n) => Idx m Source #

pattern I2 :: () => m ~ S (S (S n)) => Idx m Source #

pattern I3 :: () => m ~ S (S (S (S n))) => Idx m Source #

pattern I4 :: () => m ~ S (S (S (S (S n)))) => Idx m Source #

pattern I5 :: () => m ~ S (S (S (S (S (S n))))) => Idx m Source #

pattern I6 :: () => m ~ S (S (S (S (S (S (S n)))))) => Idx m Source #

pattern I7 :: () => m ~ S (S (S (S (S (S (S (S n))))))) => Idx m Source #

pattern I8 :: () => m ~ S (S (S (S (S (S (S (S (S n)))))))) => Idx m Source #

pattern I9 :: () => m ~ S (S (S (S (S (S (S (S (S (S n))))))))) => Idx m Source #