| 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
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?