[Agda] Info on interacting with the Agda process

Mateusz Kowalczyk fuuzetsu at fuuzetsu.co.uk
Thu Oct 23 02:02:49 CEST 2014


Hi,

Say I wanted to talk to Agda like emacs does: get all the type info,
highlighting &c &c. Is there a place where this process is documented,
notably the format that's expected both ways or is looking at the ELisp
and Haskell source the only way?

I would also ask whether we could just talk to Agda directly, cutting
out the process and parsing of the information: say we can talk to
Haskell natively, would it be viable to just talk straight to the Agda
library or would it be awkward to do so? I can imagine a much better
degree of freedom with this approach but I don't know whether it was
ever intended to be used this way. Notably, the package on Hackage says
“Note that the Agda library does not follow the package versioning
policy, because it is not intended to be used by third-party packages.”.

Thanks.

-- 
Mateusz K.


More information about the Agda mailing list