beta reduction

Stream: general

[Yury G. Kudryashov]

What is the good style to ask for beta reduction? Currently I use simp only [].

[Mario Carneiro]

I usually do the same. You can also use dsimp only []

[Mario Carneiro]

it would be good to have a tactic for this though

[Johan Commelin]

Yes, why do we have delta but not zeta and beta etc...? We could turn our proof scripts into passages from the Iliad if we had access to those tactics! Let's find out which awesome theorems Homer proved!

[Jannis Limperg]

There are non-interactive tactics head_beta, head_zeta, head_eta which perform the corresponding reduction, but only at the head of an expression. It should be easy to make variants that x-normalise a term (for x = β, ζ, η).