Zulip Chat Archive

Stream: new members

Topic: what kind of object is `brec_on`


view this post on Zulip Chris M (Aug 06 2020 at 18:31):

I just found out about brec_on, which from the tutorial I understand is used when a recursive definition doesn't just depend on the structural predecessors of a term, but on earlier "ancestors" terms as well.

Is brec_on a primitive function, without which we couldn't do such recursion? Or is it translated into something based on rec_on?

view this post on Zulip Jalex Stark (Aug 06 2020 at 18:45):

#check @bin_tree.rec_on
#check @bin_tree.brec_on
#check @bin_tree.below

I don't know what this last term below is, but I guess it is also auto-generated by inductive, and it shows up in the type signature brec_on

view this post on Zulip Reid Barton (Aug 06 2020 at 18:47):

#print will show you how they are defined (which they indeed are)

view this post on Zulip Reid Barton (Aug 06 2020 at 18:47):

I think only rec is not a definition

view this post on Zulip Jalex Stark (Aug 06 2020 at 19:03):

you mean they are not autogenerated? why does right click on bin_tree.below -> go to source take me to the definition of bin_tree?

view this post on Zulip Jalex Stark (Aug 06 2020 at 19:04):

maybe this means I should trust docs#bin_tree.below over right click go to source

view this post on Zulip Jalex Stark (Aug 06 2020 at 19:04):

the docs also don't find it, presumably because of the keyword protected that appears when you #print bin_tree.below?

view this post on Zulip Reid Barton (Aug 06 2020 at 19:05):

No they are autogenerated, of course

view this post on Zulip Reid Barton (Aug 06 2020 at 19:05):

But they are not axioms

view this post on Zulip Reid Barton (Aug 06 2020 at 19:05):

They are automatically generated definitions

view this post on Zulip Jalex Stark (Aug 06 2020 at 19:07):

okay, thanks, I am un-confused, but I'm not still not sure what Chris M's confusion is/was

view this post on Zulip Reid Barton (Aug 06 2020 at 19:09):

One thing that is confusing/surprising here is that the equation compiler always uses brec_on for structural recursion, even when you write something that looks exactly like an application of rec_on

view this post on Zulip Chris M (Aug 07 2020 at 03:17):

I wasn't confused about anything in particular, I'm just trying to get a clear model of how recursion in lean works, and it seems like it's all reduced to rec. I didn't think of using #print for some reason...

view this post on Zulip Eric Wieser (Aug 07 2020 at 08:59):

What does the b in brec_on mean?

view this post on Zulip Mario Carneiro (Aug 07 2020 at 10:46):

bounded recursion

view this post on Zulip Mario Carneiro (Aug 07 2020 at 10:47):

because it is used to compile patterns like f (n + 3) = f n but not f n = f (n / 2)


Last updated: May 16 2021 at 21:11 UTC