Docs for inductive generated functions like T.rec?

Stream: new members

[aron]

I've come across things like recursors, like here in the theorem proving docs or by someone in response to a question I asked.

But I haven't seen any real documentation about this, how it works, or what other functions and values get generated when you define an inductive type.

And unlike most things in Lean, there's no source code to view when I Cmd+click on the recursor because that just takes me to my inductive definition, not the recursor definition.

For some reason, the vscode LSP also doesn't show these functions when I dot into my type name, although once I have it written out it does know that these are valid functions

[Damiano Testa]

You can get some guidance on what gets autogenerated using whatsnew in. For instance

import Mathlib

whatsnew in
inductive X where

[aron]

Mmyeah that's definitely a useful starting point, but this still isn't very readable or offers any explanations of what I'm looking at
Screenshot 2025-01-26 at 18.01.37.png

[Kyle Miller]

There's no source code for the rec function because it's part of what inductive introduces to the environment. It has no intrinsic definition. There are some reduction rules it has as part of Lean's theory, implemented deep within the system.

There are very few cases where you might ever use a recursor directly. You're supposed to define recursive functions with a match instead. Lean compiles recursive functions to recursors automatically.