Can #check show reduction steps?

Stream: new members

[Eric Taucher]

Working through "Theorem Proving in Lean", currently in section "2.3 Function Abstraction and Evaluation".
#check is/seems to be doing Lambda Calculus reductions or Type inference
In learning Lambda Calculus the Lambda calculus reduction workbench (site) (app) was helpful in understanding the reductions used.
Does there exist some options for #check or other command that can show the reductions?

[Marcus Rossel]

I've heard other people talk about using certain "trace" functionalities of Lean for this (in the context of debugging).
I'm not sure if that would show what you expect though, as Lean's underlying calculus does more than just beta-, eta-reduction and alpha-conversion.

[Marcus Rossel]

Mario has a description of the things going on under the hood in his MS Thesis.

[Eric Taucher]

Marcus Rossel said:

I've heard other people talk about using certain "trace" functionalities of Lean for this (in the context of debugging).

To me that actually makes a lot of sense.
Instead of asking lots of questions now, I will take some time to see where that information takes me and perhaps ask more latter.

[Eric Taucher]

Marcus Rossel said:

Mario has a description of the things going on under the hood in his MS Thesis.

That is the second time in as many days that I have been directed to that. Still have not read all the way through it, now seems like the right time.

[Marcus Rossel]

@Eric Taucher I don't think you need to read all the way through. Sections 2.1-2.5 should give you a good amount of info already.

[Eric Taucher]

In an odd way this other topic is also shedding some light, namely set_option. I still have to try it but am reading the paper to the end just to have it imprinted in my memory. Much of it spilling out.