Custom eliminators

Stream: lean4

[Trebor Huang]

I somehow have the impression that Lean 4 allows you to define your own eliminators and use pattern matching with them. But I can't find the documentation. Is that a real feature or am I hallucinating like GPT3?

[Mario Carneiro]

That sounds like induction using

[Mario Carneiro]

there is also a way to register your functions as if they were using'd by default

[Mario Carneiro]

however, you probably hallucinated that there was documentation about it ;)

[Mario Carneiro]

the attribute to register custom eliminators is @[eliminator]

[Jannis Limperg]

There's also an attribute for custom patterns, I think @[match_pattern].