Hoogle Search

Within LTS Haskell 24.52 (ghc-9.10.3)

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

Exact lookup

1. setFunctionFlag :: FunctionFlag -> Bool -> QName -> TCM ()

   Agda	Agda.TypeChecking.Monad.Signature

   No documentation available.

2. setHardCompileTimeModeIfErased :: Erased -> TCM a -> TCM a

   Agda	Agda.TypeChecking.Monad.Signature

   If the first argument is Erased something, then hard compile-time mode is enabled when the continuation is run.

3. setHardCompileTimeModeIfErased' :: LensQuantity q => q -> TCM a -> TCM a

   Agda	Agda.TypeChecking.Monad.Signature

   If the quantity is "erased", then hard compile-time mode is enabled when the continuation is run. Precondition: The quantity must not be Quantity1 something.

4. setModeUnlessInHardCompileTimeMode :: Erased -> TCM a -> TCM a

   Agda	Agda.TypeChecking.Monad.Signature

   Use hard compile-time mode in the continuation if the first argument is Erased something. Use run-time mode if the first argument is NotErased something and the current mode is not hard compile-time mode.

5. setModuleCheckpoint :: ModuleName -> TCM ()

   Agda	Agda.TypeChecking.Monad.Signature

   Sets the checkpoint for the given module to the current checkpoint.

6. setMutual :: QName -> [QName] -> TCM ()

   Agda	Agda.TypeChecking.Monad.Signature

   Set the mutually recursive identifiers. TODO: This produces data of quadratic size (which has to be processed upon serialization). Presumably qs is usually short, but in some cases (for instance for generated code) it may be long. It would be better to assign a unique identifier to each SCC, and store the names separately.

7. setPolarity :: (MonadTCState m, MonadDebug m) => QName -> [Polarity] -> m ()

   Agda	Agda.TypeChecking.Monad.Signature

   Set the polarity of a definition.

8. setRunTimeModeUnlessInHardCompileTimeMode :: TCM a -> TCM a

   Agda	Agda.TypeChecking.Monad.Signature

   Use run-time mode in the continuation unless the current mode is the hard compile-time mode.

9. setSplitTree :: QName -> SplitTree -> TCM ()

   Agda	Agda.TypeChecking.Monad.Signature

   Set SplitTree of a defined function symbol.

10. setTerminates :: MonadTCState m => QName -> Bool -> m ()

    Agda	Agda.TypeChecking.Monad.Signature

    Set termination info of a defined function symbol.

Page 754 of many | Previous | Next