Agda-2.6.3.20230930: A dependently typed functional programming language and proof assistant
Safe HaskellSafe-Inferred
LanguageHaskell2010

Agda.TypeChecking.Substitute.DeBruijn

Synopsis

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

We can substitute Terms 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 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 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 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 a => DeBruijn (Named_ a) Source # 
Instance details

Defined in Agda.TypeChecking.Substitute.DeBruijn

Methods

deBruijnVar :: Int -> Named_ a Source #

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

deBruijnView :: Named_ a -> 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 #