Zulip Chat Archive

Stream: general

Topic: well_founded.fix


view this post on Zulip Kenny Lau (Jul 28 2018 at 18:35):

attribute [elab_as_eliminator] well_founded.fix

view this post on Zulip Kenny Lau (Jul 28 2018 at 18:35):

can we put this somewhere in mathlib?

view this post on Zulip Kevin Buzzard (Jul 28 2018 at 19:11):

What does it do?

view this post on Zulip Kenny Lau (Jul 28 2018 at 19:11):

well-founded recursion

view this post on Zulip Kenny Lau (Jul 28 2018 at 19:11):

oh, it makes sure that the motive is computed

view this post on Zulip Kenny Lau (Jul 28 2018 at 19:12):

you need elab_as_eliminator in things like rec_on


Last updated: May 14 2021 at 23:14 UTC