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

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

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 Methods deBruijnVar :: Int -> TTerm Source # debruijnNamedVar :: String -> Int -> TTerm Source # deBruijnView :: TTerm -> Maybe Int Source #
DeBruijn DeBruijnPattern Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods deBruijnVar :: Int -> DeBruijnPattern Source # debruijnNamedVar :: String -> Int -> DeBruijnPattern Source # deBruijnView :: DeBruijnPattern -> 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 LevelAtom Source # |
Instance details Defined in Agda.TypeChecking.Substitute.DeBruijn Methods deBruijnVar :: Int -> LevelAtom Source # debruijnNamedVar :: String -> Int -> LevelAtom Source # deBruijnView :: LevelAtom -> 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 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 Term Source # | We can substitute `Term`s 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 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 SplitPattern Source # |
Instance details Defined in Agda.TypeChecking.Coverage.Match Methods deBruijnVar :: Int -> SplitPattern Source # debruijnNamedVar :: String -> Int -> SplitPattern Source # deBruijnView :: SplitPattern -> 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 #