Hoogle Search

Within LTS Haskell 24.6 (ghc-9.10.2)

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

Exact lookup

1. data InteractionFormat

   Agda	Agda.Main

   No documentation available.

2. InteractionJson :: InteractionFormat

   Agda	Agda.Main

   --interaction-json.

3. type Interactor a = TCM () -> AbsolutePath -> TCM CheckResult -> TCM a

   Agda	Agda.Main

   No documentation available.

4. newtype InteractionId

   Agda	Agda.Syntax.Common

   No documentation available.

5. InteractionId :: Nat -> InteractionId

   Agda	Agda.Syntax.Common

   No documentation available.

6. InteractionError :: InteractionError -> TypeError

   Agda	Agda.TypeChecking.Monad.Base

   No documentation available.

7. data InteractionError

   Agda	Agda.TypeChecking.Monad.Base

   Errors raised in --interaction mode.

8. InteractionMetaBoundaries :: Set1 Range -> Warning

   Agda	Agda.TypeChecking.Monad.Base

   Do not use directly with warning

9. type InteractionOutputCallback = Response_boot TCErr TCWarning WarningsAndNonFatalErrors -> TCM ()

   Agda	Agda.TypeChecking.Monad.Base

   Callback fuction to call when there is a response to give to the interactive frontend. Note that the response is given in pieces and incrementally, so the user can have timely response even during long computations. Typical InteractionOutputCallback functions:

   • Convert the response into a String representation and print it on standard output (suitable for inter-process communication).
   • Put the response into a mutable variable stored in the closure of the InteractionOutputCallback function. (suitable for intra-process communication).

10. data InteractionPoint

    Agda	Agda.TypeChecking.Monad.Base

    Interaction points are created by the scope checker who sets the range. The meta variable is created by the type checker and then hooked up to the interaction point.

Page 14 of many | Previous | Next