DeBruijn.Idx

de Bruijn indices for well-scoped terms.

de Bruijn indices

data Idx n where

de Bruijn indices.

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

Constructors

IZ :: Idx (S n)

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

Instances

Renamable Idx

Defined in DeBruijn.Ren

Methods

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

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

RenamableA Idx

Defined in DeBruijn.Ren

Methods

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

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

Subst Idx

Defined in DeBruijn.Sub

Methods

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

Var Idx

Defined in DeBruijn.Sub

Methods

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

Show (Idx j)

Defined in DeBruijn.Idx

Methods

showsPrec :: Int -> Idx j -> ShowS

show :: Idx j -> String

showList :: [Idx j] -> ShowS

Eq (Idx n)

Defined in DeBruijn.Idx

Methods

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

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

Ord (Idx n)

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

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

Case on Idx. (compare to maybe).

idxToInt :: Idx n -> Int

Convert index to Int.

Common indices

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

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

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

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

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

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

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

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

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