Agda-2.3.2: A dependently typed functional programming language and proof assistant

Safe Haskell | None

Agda.Interaction.Highlighting.Emacs

Description

Functions which give precise syntax highlighting info to Emacs.

Synopsis

- lispifyHighlightingInfo :: HighlightingInfo -> ModuleToSource -> TCM (Lisp String)
- tests :: IO Bool

# Documentation

lispifyHighlightingInfo

Arguments

:: HighlightingInfo |
-> ModuleToSource | Must contain a mapping for every definition site's module.
-> TCM (Lisp String) |

Turns syntax highlighting information into a list of S-expressions.

tests :: IO Bool

All the properties.