Hoogle Search

Within LTS Haskell 24.28 (ghc-9.10.3)

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

  1. builtinAgdaTCMWithExpandLast :: BuiltinId

    Agda Agda.Syntax.Builtin

    No documentation available.

  2. parseLastPos :: ParseState -> !PositionWithoutFile

    Agda Agda.Syntax.Parser.Monad

    position of last token

  3. setLastPos :: PositionWithoutFile -> Parser ()

    Agda Agda.Syntax.Parser.Monad

    No documentation available.

  4. splitLast :: Induction -> Telescope -> [NamedArg DeBruijnPattern] -> TCM (Either SplitError Covering)

    Agda Agda.TypeChecking.Coverage

    Entry point from TypeChecking.Empty and Interaction.BasicOps. splitLast CoInductive is used in the refine tactics.

  5. DontExpandLast :: ExpandHidden

    Agda Agda.TypeChecking.Monad.Base

    Do not append implicit arguments.

  6. ExpandLast :: ExpandHidden

    Agda Agda.TypeChecking.Monad.Base

    Add implicit arguments in the end until type is no longer hidden Pi.

  7. ReallyDontExpandLast :: ExpandHidden

    Agda Agda.TypeChecking.Monad.Base

    Makes doExpandLast have no effect. Used to avoid implicit insertion of arguments to metavariables.

  8. eExpandLast :: Lens' TCEnv ExpandHidden

    Agda Agda.TypeChecking.Monad.Base

    No documentation available.

  9. eExpandLastBool :: Lens' TCEnv Bool

    Agda Agda.TypeChecking.Monad.Base

    No documentation available.

  10. envExpandLast :: TCEnv -> ExpandHidden

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

Page 116 of many | Previous | Next