missing documentation about agda-writer

1
votes

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

1
agda

1 Answers

1
votes

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.