[Agda] Quirk: C-c C-n thinks that some symbols are not in scope

Martin Escardo 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 
> teaching!
> 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 mailing list