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.

  1. builtinAgdaTCMAskExpandLast :: BuiltinId

    Agda Agda.Syntax.Builtin

    No documentation available.

  2. builtinAgdaTCMWithExpandLast :: BuiltinId

    Agda Agda.Syntax.Builtin

    No documentation available.

  3. parseLastPos :: ParseState -> !PositionWithoutFile

    Agda Agda.Syntax.Parser.Monad

    position of last token

  4. setLastPos :: PositionWithoutFile -> Parser ()

    Agda Agda.Syntax.Parser.Monad

    No documentation available.

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

  6. DontExpandLast :: ExpandHidden

    Agda Agda.TypeChecking.Monad.Base

    Do not append implicit arguments.

  7. ExpandLast :: ExpandHidden

    Agda Agda.TypeChecking.Monad.Base

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

  8. ReallyDontExpandLast :: ExpandHidden

    Agda Agda.TypeChecking.Monad.Base

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

  9. eExpandLast :: Lens' TCEnv ExpandHidden

    Agda Agda.TypeChecking.Monad.Base

    No documentation available.

  10. eExpandLastBool :: Lens' TCEnv Bool

    Agda Agda.TypeChecking.Monad.Base

    No documentation available.

Page 117 of many | Previous | Next