trace in #reduce

Stream: lean4

[Nir Paz]

I want to use something like trace.profiler to see how a definition was reduced with #reduce, and set_option trace.profiler true doesn't work for this. How can I see how something was reduced?

[Henrik Böving]

I dont think you can currently trace this facility. Do you have a particular reason for wanting this?

[Nir Paz]

I was following the construction of a term with a non terminating reduction from a paper and wanted to see the trace to understand lean's reduction process better. If anyone's interested:

namespace Hidden

def False : Prop := ∀ P : Prop, P
def Not : Prop → Prop := λ P ↦ (P → False)
def True : Prop := Not False

def delta : True := λ z ↦ z True z
def omega : Not (∀ P Q : Prop, P = Q) := λ h A ↦ cast (h True A) delta
def Omega : Not (∀ P Q : Prop, P = Q) := λ h ↦ delta (omega h)

#reduce Omega -- maximum depth reached