[Agda] How to make chain of reasoning explicit in Agda

[Herminie Pagel]

Hi Agda Community,

when viewing the normalized goal of a given clause, i am wondering how to
get the reasoning steps that Agda performs to decuce the current goal from
the initial result to be proven.

More precisely, which definitionally equalities and syntactic precedences
are being applied, in which order and the resulting intermediate
expressions that lead to the current goal shown by C-c C-. in a given hole.

best, herminie
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20190614/d24784b1/attachment.html>