what is `elab_as_elim`

Stream: general

[Asei Inoue]

what is [elab_as_elim] attribute? what does this attribute? what is the difference when I add this attribute to something...?

[Kevin Buzzard]

It changes the way the declaration is elaborated. I don't know the technical details but presumably the idea is that with the tag, Lean is more prepared to have a good guess at the type of the motive which the user means, even though this typically means solving a higher-order unification problem.

[Asei Inoue]

is there an example ?

[Kevin Buzzard]

Sure, search mathlib for the attribute, then remove it from something and see what breaks.

[Aaron Liu]

@[elab_as_elim] registers the declaration as an eliminator. Eliminators have special support for filling in the motives automatically with syntactic replacement instead of using second-order unification. By default, .rec, .recOn, .casesOn, .brecOn are all eliminators.

[Kevin Buzzard]

Things we want to use as recursors (i.e. stuff we want to use to do induction) is what is being tagged.

[Asei Inoue]

Thank you!

[Kyle Miller]

In general, @[elab_as_elim] is for declarations whose return type is of the form p x1 x2 ... xn, and during elaboration you want p to be solved for using the expected type. The expressions x1 through xn can be arbitrary expressions. To solve for p, xn through x1 are replaced by variables in that order; the result is the body for p. (This process can fail, and you may get a "motive not type correct" error. That's when the expression for p is ill-typed.) The elaborator will throw an error if there is no expected type.

There are a couple of other different rules for how these are elaborated. It eagerly elaborates all arguments that appear in x1 through xn. These are like "major premises", using eliminator terminology. The remaining arguments are "minor premises", and and elaboration for those is deferred until after p is computed.

@[elab_as_elim] at this point is only loosely related to eliminators, but every eliminator uses this elaboration procedure.

This attribute shouldn't be confused with @[induction_eliminator] or @[cases_eliminator], which are for configuring which induction or cases principle should be used for the induction and cases tactics.