| Safe Haskell | Safe-Inferred |
|---|---|
| Language | Haskell2010 |
Agda.Convert
Synopsis
- responseAbbr :: IsString a => Response -> a
- serialize :: Lisp String -> String
- fromResponse :: Response -> TCM Response
- fromHighlightingInfo :: HighlightingInfo -> RemoveTokenBasedHighlighting -> HighlightingMethod -> ModuleToSource -> TCM Response
- fromDisplayInfo :: DisplayInfo -> TCM DisplayInfo
- lispifyGoalSpecificDisplayInfo :: InteractionId -> GoalDisplayInfo -> TCM DisplayInfo
- showInfoError :: Info_Error -> TCM String
- explainWhyInScope :: String -> FilePath -> Maybe LocalVar -> [AbstractName] -> [AbstractModule] -> TCM Doc
- prettyResponseContexts :: InteractionId -> Bool -> [ResponseContextEntry] -> TCM Doc
- prettyResponseContext :: InteractionId -> ResponseContextEntry -> TCM [(String, Doc)]
- renderResponseContext :: InteractionId -> ResponseContextEntry -> TCM [Block]
- prettyTypeOfMeta :: Rewrite -> InteractionId -> TCM (Inlines, String)
- prettyTimed :: CPUTime -> Doc
Documentation
responseAbbr :: IsString a => Response -> a Source #
fromResponse :: Response -> TCM Response Source #
fromHighlightingInfo :: HighlightingInfo -> RemoveTokenBasedHighlighting -> HighlightingMethod -> ModuleToSource -> TCM Response Source #
fromDisplayInfo :: DisplayInfo -> TCM DisplayInfo Source #
lispifyGoalSpecificDisplayInfo :: InteractionId -> GoalDisplayInfo -> TCM DisplayInfo Source #
showInfoError :: Info_Error -> TCM String Source #
Serializing Info_Error
explainWhyInScope :: String -> FilePath -> Maybe LocalVar -> [AbstractName] -> [AbstractModule] -> TCM Doc Source #
prettyResponseContexts Source #
Arguments
| :: InteractionId | Context of this meta-variable. |
| -> Bool | Print the elements in reverse order? |
| -> [ResponseContextEntry] | |
| -> TCM Doc |
Pretty-prints the context of the given meta-variable.
prettyResponseContext Source #
Arguments
| :: InteractionId | Context of this meta-variable. |
| -> ResponseContextEntry | |
| -> TCM [(String, Doc)] |
Pretty-prints the context of the given meta-variable.
renderResponseContext Source #
Arguments
| :: InteractionId | Context of this meta-variable. |
| -> ResponseContextEntry | |
| -> TCM [Block] |
Render the context of the given meta-variable.
prettyTypeOfMeta :: Rewrite -> InteractionId -> TCM (Inlines, String) Source #
Pretty-prints the type of the meta-variable.
prettyTimed :: CPUTime -> Doc Source #
Prefix prettified CPUTime with "Time:"