Agda.TypeChecking.Substitute.DeBruijn · Agda-2.7.0.1

classclass DeBruijn a where

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

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?

Instances10DeBruijn, …

DeBruijn BraveTermDefined in Agda-2.7.0.1 · Agda.TypeChecking.Substitute · orphan
DeBruijn DBPatVarDefined in Agda-2.7.0.1 · Agda.TypeChecking.Substitute.DeBruijn
DeBruijn LevelDefined in Agda-2.7.0.1 · Agda.TypeChecking.Substitute.DeBruijn
DeBruijn PlusLevelDefined in Agda-2.7.0.1 · Agda.TypeChecking.Substitute.DeBruijn
DeBruijn TermDefined in Agda-2.7.0.1 · Agda.TypeChecking.Substitute.DeBruijn
We can substitute Terms for variables.
DeBruijn TTermDefined in Agda-2.7.0.1 · Agda.Compiler.Treeless.Subst · orphan
DeBruijn SplitPatVarDefined in Agda-2.7.0.1 · Agda.TypeChecking.Coverage.Match
DeBruijn NLPatDefined in Agda-2.7.0.1 · Agda.TypeChecking.Substitute · orphan
DeBruijn a => DeBruijn (Named_ a)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Substitute.DeBruijn
DeBruijn a => DeBruijn (Pattern' a)Defined in Agda-2.7.0.1 · Agda.TypeChecking.Substitute · orphan