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

[Martin Escardo]

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.

Best,
Martin