Agda.TypeChecking.Substitute.DeBruijn

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 LevelAtom

Methods

deBruijnVar :: Int -> LevelAtom

debruijnNamedVar :: String -> Int -> LevelAtom

deBruijnView :: LevelAtom -> Maybe Int

DeBruijn PlusLevel

Methods

deBruijnVar :: Int -> PlusLevel

debruijnNamedVar :: String -> Int -> PlusLevel

deBruijnView :: PlusLevel -> Maybe Int

DeBruijn Level

Methods

deBruijnVar :: Int -> Level

debruijnNamedVar :: String -> Int -> Level

deBruijnView :: Level -> Maybe Int

DeBruijn Term

We can substitute Terms for variables.

Methods

deBruijnVar :: Int -> Term

debruijnNamedVar :: String -> Int -> Term

deBruijnView :: Term -> Maybe Int