Hoogle Search

Within LTS Haskell 24.36 (ghc-9.10.3)

Note that Stackage only displays results for the latest LTS and Nightly snapshot. Learn more.

Exact lookup

1. getContextVars' :: MonadTCEnv m => m [(Int, Dom Name)]

   Agda	Agda.TypeChecking.Monad.Context

   No documentation available.

2. 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.

3. wakeIrrelevantVars :: MonadTCEnv tcm => tcm a -> tcm a

   Agda	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.

4. class NLPatVars a

   Agda	Agda.TypeChecking.Rewriting.NonLinPattern

   Gather the set of pattern variables of a non-linear pattern

5. nlPatVars :: NLPatVars a => a -> IntSet

   Agda	Agda.TypeChecking.Rewriting.NonLinPattern

   No documentation available.

6. nlPatVarsUnder :: NLPatVars a => Int -> a -> IntSet

   Agda	Agda.TypeChecking.Rewriting.NonLinPattern

   No documentation available.

7. checkSortOfSplitVar :: (MonadTCM m, PureTCM m, MonadError TCErr m, LensSort a, PrettyTCM a, LensSort ty, PrettyTCM ty) => DataOrRecord -> a -> Telescope -> Maybe ty -> m ()

   Agda	Agda.TypeChecking.Rules.LHS

   No documentation available.

8. getVarType :: Int -> UnifyState -> Dom Type

   Agda	Agda.TypeChecking.Rules.LHS.Unify.Types

   Get the type of the i'th variable in the given state

9. getVarTypeUnraised :: Int -> UnifyState -> Dom Type

   Agda	Agda.TypeChecking.Rules.LHS.Unify.Types

   No documentation available.

10. expandEnvironmentVariables :: String -> IO String

    Agda	Agda.Utils.Environment

    No documentation available.

Page 55 of many | Previous | Next