Agda-2.6.1: A dependently typed functional programming language and proof assistant

Safe HaskellNone
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
DeBruijn TTerm Source # 
Instance details

Defined in Agda.Compiler.Treeless.Subst

DeBruijn DBPatVar Source # 
Instance details

Defined in Agda.TypeChecking.Substitute.DeBruijn

DeBruijn BraveTerm Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

DeBruijn LevelAtom Source # 
Instance details

Defined in Agda.TypeChecking.Substitute.DeBruijn

DeBruijn PlusLevel Source # 
Instance details

Defined in Agda.TypeChecking.Substitute.DeBruijn

DeBruijn Level Source # 
Instance details

Defined in Agda.TypeChecking.Substitute.DeBruijn

DeBruijn Term Source #

We can substitute Terms for variables.

Instance details

Defined in Agda.TypeChecking.Substitute.DeBruijn

DeBruijn NLPat Source # 
Instance details

Defined in Agda.TypeChecking.Substitute

DeBruijn SplitPatVar Source # 
Instance details

Defined in Agda.TypeChecking.Coverage.Match

DeBruijn a => DeBruijn (Pattern' a) Source # 
Instance details

Defined in Agda.TypeChecking.Substitute