Safe Haskell	Unsafe
Language	Haskell2010

DeBruijn.Internal.Idx

Contents

Description

de Bruijn indices for well-scoped terms.

Synopsis

newtype Idx j where
- UnsafeIdx Int
- pattern IZ :: () => m ~ S n => Idx m
- pattern IS :: () => m ~ S n => Idx n -> Idx m
absurdIdx :: Idx EmptyCtx -> a
unIdx :: a -> (Idx n -> a) -> Idx (S n) -> a
idxToInt :: Idx ctx -> Int
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

de Bruijn indices

newtype Idx j Source #

de Bruijn indices.

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

Constructors

Bundled Patterns

pattern IZ :: () => m ~ S n => Idx m
pattern IS :: () => m ~ S n => Idx n -> Idx m

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.Internal.Idx Methods showsPrec :: Int -> Idx j -> ShowS # show :: Idx j -> String # showList :: [Idx j] -> ShowS #
Eq (Idx n) Source #
Instance details Defined in DeBruijn.Internal.Idx Methods (==) :: Idx n -> Idx n -> Bool # (/=) :: Idx n -> Idx n -> Bool #
Ord (Idx n) Source #
Instance details Defined in DeBruijn.Internal.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 #

Derive anything from index into empty scope.

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

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

Case on Idx. (compare to maybe).

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 #