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).
I found a solution: Ctrl-C Ctrl-N in agda-mode allows inputting an expression and then prints the evaluated result.