agdaagda-mode

Equivalent of Coq's `Eval` for Agda


Coq has an Eval command that you can use to have the type-checker evaluate an expression and print it to the console. Is there an equivalent to this in Agda? In particular, I'd like to avoid actually compiling and executing the program. I just want to introspect a value to make sure my code is working (and help me understand it better) before I go to the effort of writing proofs.

It's fine if the solution involves agda-mode (as compared to Coq, where it's part of the language).


Solution

  • I found a solution: Ctrl-C Ctrl-N in agda-mode allows inputting an expression and then prints the evaluated result.