False claim of `C-c C-a` usability in Lambda chapter.

plfa / plfa.github.io

An introduction to programming language theory in Agda

https://plfa.github.io

Creative Commons Attribution 4.0 International

1.37k stars 315 forks source link

False claim of `C-c C-a` usability in Lambda chapter. #517

Open capn-freako opened 4 years ago

capn-freako commented 4 years ago

At the very end of the Interacting with Agda section of the Lambda chapter of Part 2 of PLFA, it is claimed:

The entire process can be automated using Agsy, invoked with C-c C-a.

However, when I try this I'm told:

Not implemented: The Agda synthesizer (Agsy) does not support literals yet

wenkokke commented 2 years ago

Is this still true using the most recent version of Agda?

dunhamsteve commented 10 months ago

This error still occurs for me with Agda 2.6.3-b499d12. Repeatedly doing C-c C-r works, but C-c C-a says "Not implemented: The Agda synthesizer (Agsy) does not support literals yet". I'm not sure what "literals" refers to.

I ran into this error a number of times working through the file before I got to the note near the end saying that it should work.