Zulip Chat Archive

Stream: general

Topic: beta reduction

Yury G. Kudryashov (Apr 09 2020 at 02:31):

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

Mario Carneiro (Apr 09 2020 at 02:34):

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

Mario Carneiro (Apr 09 2020 at 02:34):

it would be good to have a tactic for this though

Johan Commelin (Apr 09 2020 at 05:25):

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 (Apr 09 2020 at 12:50):

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 = β, ζ, η).

Last updated: Aug 03 2023 at 10:10 UTC