Hoogle Search
Within LTS Haskell 24.12 (ghc-9.10.3)
Note that Stackage only displays results for the latest LTS and Nightly snapshot. Learn more.
setLastPos :: PositionWithoutFile -> Parser ()Agda Agda.Syntax.Parser.Monad No documentation available.
-
Agda Agda.TypeChecking.Coverage Entry point from TypeChecking.Empty and Interaction.BasicOps. splitLast CoInductive is used in the refine tactics.
DontExpandLast :: ExpandHiddenAgda Agda.TypeChecking.Monad.Base Do not append implicit arguments.
-
Agda Agda.TypeChecking.Monad.Base Add implicit arguments in the end until type is no longer hidden Pi.
ReallyDontExpandLast :: ExpandHiddenAgda Agda.TypeChecking.Monad.Base Makes doExpandLast have no effect. Used to avoid implicit insertion of arguments to metavariables.
eExpandLast :: Lens' TCEnv ExpandHiddenAgda Agda.TypeChecking.Monad.Base No documentation available.
eExpandLastBool :: Lens' TCEnv BoolAgda Agda.TypeChecking.Monad.Base No documentation available.
envExpandLast :: TCEnv -> ExpandHiddenAgda Agda.TypeChecking.Monad.Base When type-checking an alias f=e, we do not want to insert hidden arguments in the end, because these will become unsolved metas.
isDontExpandLast :: ExpandHidden -> BoolAgda Agda.TypeChecking.Monad.Base No documentation available.
isExpandLast :: ExpandHidden -> BoolAgda Agda.TypeChecking.Monad.Base No documentation available.