Hoogle Search

Within LTS Haskell 24.48 (ghc-9.10.3)

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

Exact lookup

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

2. forcePiUsingInjectivity :: Type -> TCM Type

   Agda	Agda.TypeChecking.Injectivity

   No documentation available.

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

4. formatDebugMessage :: MonadDebug m => VerboseKey -> VerboseLevel -> TCM Doc -> m String

   Agda	Agda.TypeChecking.Monad.Debug

   No documentation available.

5. forceEtaExpandRecord :: (HasConstInfo m, MonadDebug m, ReadTCState m, MonadError TCErr m) => QName -> Args -> Term -> m (Telescope, Args)

   Agda	Agda.TypeChecking.Records

   Eta expand a record regardless of whether it's an eta-record or not.

6. forceSort :: Type -> TCM Sort

   Agda	Agda.TypeChecking.Rules.Data

   Ensure that the type is a sort. If it is not directly a sort, compare it to a newSortMetaBelowInf.

7. forA :: (Traversable t, Applicative f) => t a -> (a -> f b) -> f (t b)

   Agda	Agda.Utils.Applicative

   Better name for for.

8. forMaybe :: [a] -> (a -> Maybe b) -> [b]

   Agda	Agda.Utils.Maybe

   Version of mapMaybe with different argument ordering.

9. forMaybe :: [a] -> (a -> Maybe b) -> [b]

   Agda	Agda.Utils.Maybe.Strict

   Version of mapMaybe with different argument ordering.

10. forM :: (Traversable t, Monad m) => t a -> (a -> m b) -> m (t b)

    Agda	Agda.Utils.Monad

    forM is mapM with its arguments flipped. For a version that ignores the results see forM_.

Page 150 of many | Previous | Next