In Coq, if I am unsure how a definition
foo is defined, I can use the command
Print foo. to inspect what
foo looks like. If I am not satisfied with this, I can also build a dummy goal, say
Goal foo = foo. and then use tactics such as
unfold to gradually unroll the definition of
foo (say I do first
unfold foo., then I see another term
bar so I can
unfold bar., and so forth).
Is it possible to perform a similar task in Agda? I am aware of the ability to "normalize a term" (C-c C-n), and I could also look at the source Agda definition, but in my case I would very much like to inspect the body of a definition after elaboration, but before any form of normalization.
I also considered using reflection, in particular the
getDefinition operation, but unfortunately this gives a value of type
Definition only under the type-checking monad, and as far as I can tell there is no direct way to inspect this value.