Hoogle Search
Within LTS Haskell 24.18 (ghc-9.10.3)
Note that Stackage only displays results for the latest LTS and Nightly snapshot. Learn more.
primAgdaPatVar :: (HasBuiltins m, MonadError TCErr m, MonadTCEnv m, ReadTCState m) => m TermAgda Agda.TypeChecking.Monad.Builtin No documentation available.
contextVars :: Context -> [(Int, Dom Name)]Agda Agda.TypeChecking.Monad.Context No documentation available.
contextVars' :: Context -> [(Int, Dom Name)]Agda Agda.TypeChecking.Monad.Context No documentation available.
getContextVars :: MonadTCEnv m => m [(Int, Dom Name)]Agda Agda.TypeChecking.Monad.Context No documentation available.
getContextVars' :: MonadTCEnv m => m [(Int, Dom Name)]Agda Agda.TypeChecking.Monad.Context No documentation available.
getVarInfo :: (MonadDebug m, MonadTCEnv m) => Name -> m (Term, Dom Type)Agda Agda.TypeChecking.Monad.Context Get the term corresponding to a named variable. If it is a lambda bound variable the deBruijn index is returned and if it is a let bound variable its definition is returned.
wakeIrrelevantVars :: MonadTCEnv tcm => tcm a -> tcm aAgda Agda.TypeChecking.Monad.Modality Wake up irrelevant variables and make them relevant. This is used when type checking terms in a hole, in which case you want to be able to (for instance) infer the type of an irrelevant variable. In the course of type checking an irrelevant function argument applyRelevanceToContext is used instead, which also sets the context relevance to Irrelevant. This is not the right thing to do when type checking interactively in a hole since it also marks all metas created during type checking as irrelevant (issue #2568). Also set the current quantity to 0.
-
Agda Agda.TypeChecking.Rewriting.NonLinPattern Gather the set of pattern variables of a non-linear pattern
nlPatVars :: NLPatVars a => a -> IntSetAgda Agda.TypeChecking.Rewriting.NonLinPattern No documentation available.
nlPatVarsUnder :: NLPatVars a => Int -> a -> IntSetAgda Agda.TypeChecking.Rewriting.NonLinPattern No documentation available.