## Stream: new members

### Topic: what kind of object is brec_on

#### 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?

#### 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

#### Reid Barton (Aug 06 2020 at 18:47):

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

#### Reid Barton (Aug 06 2020 at 18:47):

I think only rec is not a definition

#### 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?

#### Jalex Stark (Aug 06 2020 at 19:04):

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

#### 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?

#### Reid Barton (Aug 06 2020 at 19:05):

No they are autogenerated, of course

#### Reid Barton (Aug 06 2020 at 19:05):

But they are not axioms

#### Reid Barton (Aug 06 2020 at 19:05):

They are automatically generated definitions

#### 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

#### 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

#### 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...

#### Eric Wieser (Aug 07 2020 at 08:59):

What does the b in brec_on mean?

#### Mario Carneiro (Aug 07 2020 at 10:46):

bounded recursion

#### 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