Hoogle Search

Within LTS Haskell 24.35 (ghc-9.10.3)

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

  1. formatLibError :: [AgdaLibFile] -> LibError -> Doc

    Agda Agda.Interaction.Library.Base

    Pretty-print LibError.

  2. formatLibErrors :: LibErrors -> Doc

    Agda Agda.Interaction.Library.Base

    Pretty-print LibErrors.

  3. formatLibPositionInfo :: LibPositionInfo -> LibParseError -> Doc

    Agda Agda.Interaction.Library.Base

    Compute a position position prefix. Depending on the error to be printed, it will

    • either give the name of the libraries file and a line inside it,
    • or give the name of the .agda-lib file.

  4. forgetLoneSigs :: Nice ()

    Agda Agda.Syntax.Concrete.Definitions.Monad

    No documentation available.

  5. forallQ :: Doc

    Agda Agda.Syntax.Concrete.Glyph

    No documentation available.

  6. forallPi :: List1 LamBinding -> Expr -> Expr

    Agda Agda.Syntax.Parser.Helpers

    Build a forall pi (forall x y z -> ...)

  7. forallFaceMaps :: MonadConversion m => Term -> (IntMap Bool -> Blocker -> Term -> m a) -> (IntMap Bool -> Substitution -> m a) -> m [a]

    Agda Agda.TypeChecking.Conversion

    No documentation available.

  8. forceNotFree :: (ForceNotFree a, Reduce a, MonadReduce m) => IntSet -> a -> m (IntMap IsFree, a)

    Agda Agda.TypeChecking.Free.Reduce

    Try to enforce a set of variables not occurring in a given type. Returns a possibly reduced version of the type and for each of the given variables whether it is either not free, or maybe free depending on some metavariables.

  9. forcePiUsingInjectivity :: Type -> TCM Type

    Agda Agda.TypeChecking.Injectivity

    No documentation available.

  10. forkTCM :: TCM () -> TCM ()

    Agda Agda.TypeChecking.Monad.Base

    Runs the given computation in a separate thread, with a copy of the current state and environment. Note that Agda sometimes uses actual, mutable state. If the computation given to forkTCM tries to modify this state, then bad things can happen, because accesses are not mutually exclusive. The forkTCM function has been added mainly to allow the thread to read (a snapshot of) the current state in a convenient way. Note also that exceptions which are raised in the thread are not propagated to the parent, so the thread should not do anything important.

Page 149 of many | Previous | Next