Reflexive inductives

Stream: lean4

[Gabriel Barreto]

There's a field isReflexive : Bool in the struct InductiveVal here but there's no explanation of what it is. I couldn't find it in the manual either. It would be very much appreciated if anyone could explain this

[Kyle Miller]

If it helps, I found this: https://github.com/leanprover/lean4/blob/7850dc023b004443cca2e1ef937a019f9eb6a2c2/src/kernel/inductive.cpp#L287

[Gabriel Barreto]

Awesome, that helps a lot