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

[James Wood]

I've been idly thinking about the design of a hole-based REPL for some 
time. I've jotted down some design points on the issue tracker ( 
https://github.com/agda/agda/issues/5778 ). Anyone interested, let us 
know whether this goes towards solving some of your problems.

Regards,
James

On 04/02/2022 08:49, Martin Escardo wrote:
> CAUTION: This email originated outside the University. Check before 
> clicking links or attachments.
> 
> 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
> 
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda 
>