[Agda] Agda on GitHub Atom

Balaji Rao R balaji at raobalaji.com
Sat Apr 26 15:27:36 CEST 2014


On 26-Apr-2014, at 0:09, Nils Anders Danielsson <nad at cse.gu.se> wrote:

> On 2014-04-14 20:09, Balaji Rao R wrote:
>> I’ve seen that there are various files in Interaction/Highlighting,
>> for example. I was looking for some broad guidelines regarding which
>> file does what, just to help me get started.
> 
> If your goal is to use highlighting information, then the starting point
> may be the type HighlightingInfo in
> Agda.Interaction.Highlighting.Precise. The type checker stores
> highlighting info in the state. For an example of how one can use the
> highlighting info, take a look at, say,
> Agda.Interaction.Highlighting.HTML.generateHTML, which is called from
> Agda.Main.

Great. Thanks for the info!

- Balaji


More information about the Agda mailing list