<div dir="ltr"><div>Hi Agda Community,</div><div><br></div><div>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.</div><div><br></div><div>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.<br></div><div><br></div><div>best, herminie<br></div></div>