Zulip Chat Archive
Stream: general
Topic: well_founded.fix
Kenny Lau (Jul 28 2018 at 18:35):
attribute [elab_as_eliminator] well_founded.fix
Kenny Lau (Jul 28 2018 at 18:35):
can we put this somewhere in mathlib?
Kevin Buzzard (Jul 28 2018 at 19:11):
What does it do?
Kenny Lau (Jul 28 2018 at 19:11):
well-founded recursion
Kenny Lau (Jul 28 2018 at 19:11):
oh, it makes sure that the motive is computed
Kenny Lau (Jul 28 2018 at 19:12):
you need elab_as_eliminator in things like rec_on
Last updated: Dec 20 2023 at 11:08 UTC