Agda-2.8.0: 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

(deBruijnVar | deBruijnNamedVar), 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

Instances details

DeBruijn BraveTerm Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods deBruijnVar :: Int -> BraveTerm Source # deBruijnNamedVar :: String -> Int -> BraveTerm Source # deBruijnView :: BraveTerm -> 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 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 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 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 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 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 #
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 a => DeBruijn (Named_ a) Source # |
Instance details Defined in Agda.TypeChecking.Substitute.DeBruijn Methods deBruijnVar :: Int -> Named_ a Source # deBruijnNamedVar :: String -> Int -> Named_ a Source # deBruijnView :: Named_ a -> Maybe Int Source #
DeBruijn a => DeBruijn (Pattern' a) Source # |
Instance details Defined in Agda.TypeChecking.Substitute Methods deBruijnVar :: Int -> Pattern' a Source # deBruijnNamedVar :: String -> Int -> Pattern' a Source # deBruijnView :: Pattern' a -> Maybe Int Source #