[Agda] Quirk: C-c C-n thinks that some symbols are not in scope
m.escardo at cs.bham.ac.uk
Fri Feb 4 09:49:54 CET 2022
On 02/02/2022 11:19, Thorsten Altenkirch wrote:
> This is really bad from a paedagogical perspective if you use agda for
> Is there nobody who could implement a read-eval-print loop for agda? It
> shouldn’t be that difficult?
Yes, I agree. I am teaching Agda to 3rd year undergrads, and this would
be very useful. These students did Haskell in the 2nd year and they miss
something like ghci.
More information about the Agda