what kind of object is `brec_on`

Stream: new members

[Chris M]

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]

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

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

[Reid Barton]

I think only rec is not a definition

[Jalex Stark]

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]

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

[Jalex Stark]

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

[Reid Barton]

No they are autogenerated, of course

[Reid Barton]

But they are not axioms

[Reid Barton]

They are automatically generated definitions

[Jalex Stark]

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

[Reid Barton]

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]

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]

What does the b in brec_on mean?

[Mario Carneiro]

bounded recursion

[Mario Carneiro]

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