Safe Haskell	None
Language	Haskell2010

Agda.TypeChecking.Substitute.DeBruijn

Synopsis

class DeBruijn a where

Documentation

class DeBruijn a where #

Things we can substitute for a variable. Needs to be able to represent variables, e.g. for substituting under binders.

Minimal complete definition

deBruijnView

Methods

deBruijnVar :: Int -> a #

Produce a variable without name suggestion.

debruijnNamedVar :: String -> Int -> a #

Produce a variable with name suggestion.

deBruijnView :: a -> Maybe Int #

Are we dealing with a variable? If yes, what is its index?

Instances

DeBruijn TTerm #
Instance details Defined in Agda.Compiler.Treeless.Subst Methods deBruijnVar :: Int -> TTerm # debruijnNamedVar :: String -> Int -> TTerm # deBruijnView :: TTerm -> Maybe Int #
DeBruijn DeBruijnPattern #
Instance details Defined in Agda.TypeChecking.Substitute Methods deBruijnVar :: Int -> DeBruijnPattern # debruijnNamedVar :: String -> Int -> DeBruijnPattern # deBruijnView :: DeBruijnPattern -> Maybe Int #
DeBruijn LevelAtom #
Instance details Defined in Agda.TypeChecking.Substitute.DeBruijn Methods deBruijnVar :: Int -> LevelAtom # debruijnNamedVar :: String -> Int -> LevelAtom # deBruijnView :: LevelAtom -> Maybe Int #
DeBruijn PlusLevel #
Instance details Defined in Agda.TypeChecking.Substitute.DeBruijn Methods deBruijnVar :: Int -> PlusLevel # debruijnNamedVar :: String -> Int -> PlusLevel # deBruijnView :: PlusLevel -> Maybe Int #
DeBruijn Level #
Instance details Defined in Agda.TypeChecking.Substitute.DeBruijn Methods deBruijnVar :: Int -> Level # debruijnNamedVar :: String -> Int -> Level # deBruijnView :: Level -> Maybe Int #
DeBruijn Term #	We can substitute `Term`s for variables.
Instance details Defined in Agda.TypeChecking.Substitute.DeBruijn Methods deBruijnVar :: Int -> Term # debruijnNamedVar :: String -> Int -> Term # deBruijnView :: Term -> Maybe Int #
DeBruijn NLPat #
Instance details Defined in Agda.TypeChecking.Substitute Methods deBruijnVar :: Int -> NLPat # debruijnNamedVar :: String -> Int -> NLPat # deBruijnView :: NLPat -> Maybe Int #
DeBruijn SplitPattern #
Instance details Defined in Agda.TypeChecking.Coverage.Match Methods deBruijnVar :: Int -> SplitPattern # debruijnNamedVar :: String -> Int -> SplitPattern # deBruijnView :: SplitPattern -> Maybe Int #