Agda-2.5.1.2: A dependently typed functional programming language and proof assistant
Agda.TypeChecking.Substitute.Pattern
Contents
fromPatternSubstitution :: PatternSubstitution -> Substitution Source #
applyPatSubst :: Subst Term a => PatternSubstitution -> a -> a Source #
Methods
debruijnVar :: Int -> DeBruijnPattern Source #
debruijnNamedVar :: String -> Int -> DeBruijnPattern Source #
debruijnView :: DeBruijnPattern -> Maybe Int Source #
applySubst :: Substitution' DeBruijnPattern -> DeBruijnPattern -> DeBruijnPattern Source #