Reputation: 233
I've installed agda-writer, since the agda-mode for emacs won't work for me (doesn't do UTF8 characters, doesn't do syntax highlighting...??)
Installing agda-writer was dead easy, but I can't find any documentation, and i find myself unable to do the most basic tasks:
-- how do you perform type-checking? (seems like the most fundamental thing you might want agda to do for you...)
-- how do you turn syntax highlighting on?
-- how do you set the preferences for the standard library to work? (in other words, what is the path to the bundled standard library?)
Basically, the only thing i can do is to try and "compile"; of course this fails because I haven't got haskell installed, but at it least it triggers both syntax highlighting and type-checking (????)
I'm on Mojave.
Any help appreciated.
thanks, Pierre
Upvotes: 1
Views: 41
Reputation: 233
Answering partially my own question: typechecking+syntax highlighting is called "loading" in agda-write (as it is in other contexts, apparently). It's in the "actions" menu. I had assumed "load" was the same as "open the file"...
I still don't know about the standard library.
Upvotes: 1