[Agda] Quirk: C-c C-n thinks that some symbols are not in scope
james.wood.100 at strath.ac.uk
Fri Feb 4 13:48:42 CET 2022
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.
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
>> 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.
> Agda mailing list
> Agda at lists.chalmers.se
More information about the Agda