Safe Haskell	None
Language	Haskell2010

Agda.TypeChecking.Substitute.DeBruijn

Synopsis

class DeBruijn a where
- deBruijnVar :: Int -> a
- debruijnNamedVar :: String -> Int -> a
- deBruijnView :: a -> Maybe Int

Documentation

class DeBruijn a where Source #

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 Source #

Produce a variable without name suggestion.

debruijnNamedVar :: String -> Int -> a Source #

Produce a variable with name suggestion.

deBruijnView :: a -> Maybe Int Source #

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

Instances

Instances details

DeBruijn TTerm Source #
Instance details Defined in Agda.Compiler.Treeless.Subst Methods deBruijnVar :: Int -> TTerm Source # debruijnNamedVar :: String -> Int -> TTerm Source # deBruijnView :: TTerm -> Maybe Int Source #
DeBruijn DBPatVar Source #
Instance details Defined in Agda.TypeChecking.Substitute.DeBruijn Methods deBruijnVar :: Int -> DBPatVar Source # debruijnNamedVar :: String -> Int -> DBPatVar Source # deBruijnView :: DBPatVar -> Maybe Int Source #
DeBruijn BraveTerm Source #
Instance details Defined in Agda.TypeChecking.Substitute Methods deBruijnVar :: Int -> BraveTerm Source # debruijnNamedVar :: String -> Int -> BraveTerm Source # deBruijnView :: BraveTerm -> Maybe Int Source #
DeBruijn PlusLevel Source #
Instance details Defined in Agda.TypeChecking.Substitute.DeBruijn Methods deBruijnVar :: Int -> PlusLevel Source # debruijnNamedVar :: String -> Int -> PlusLevel Source # deBruijnView :: PlusLevel -> Maybe Int Source #
DeBruijn Level Source #
Instance details Defined in Agda.TypeChecking.Substitute.DeBruijn Methods deBruijnVar :: Int -> Level Source # debruijnNamedVar :: String -> Int -> Level Source # deBruijnView :: Level -> Maybe Int Source #
DeBruijn Term Source #	We can substitute `Term`s for variables.
Instance details Defined in Agda.TypeChecking.Substitute.DeBruijn Methods deBruijnVar :: Int -> Term Source # debruijnNamedVar :: String -> Int -> Term Source # deBruijnView :: Term -> Maybe Int Source #
DeBruijn NLPat Source #
Instance details Defined in Agda.TypeChecking.Substitute Methods deBruijnVar :: Int -> NLPat Source # debruijnNamedVar :: String -> Int -> NLPat Source # deBruijnView :: NLPat -> Maybe Int Source #
DeBruijn SplitPatVar Source #
Instance details Defined in Agda.TypeChecking.Coverage.Match Methods deBruijnVar :: Int -> SplitPatVar Source # debruijnNamedVar :: String -> Int -> SplitPatVar Source # deBruijnView :: SplitPatVar -> Maybe Int Source #
DeBruijn a => DeBruijn (Pattern' a) Source #
Instance details Defined in Agda.TypeChecking.Substitute Methods deBruijnVar :: Int -> Pattern' a Source # debruijnNamedVar :: String -> Int -> Pattern' a Source # deBruijnView :: Pattern' a -> Maybe Int Source #