beta_reduce

Stream: mathlib4

[Patrick Massot]

Is there a term elaborator version of the beta_reduce tactic?

[Kyle Miller]

There's a one-step one that only beta reduces the head expression. It's meant to be used like beta% f x y z where f might be a lambda expression. (I forgot it was delegated to me, and I just put it on the queue: #7207)

[Patrick Massot]

Thanks!