fix: make elabAsElim aware of explicit motive arguments

[kmill]

Some eliminators (such as False.rec) have an explicit motive argument. The elabAsElim elaborator assumed that all motives are implicit.

If the explicit motive argument is _, then it uses the elab-as-elim procedure, and otherwise it falls back to the standard app elaborator.

Furthermore, if an explicit elaborator is not provided, it falls back to treating the elaborator as being implicit, which is convenient for writing h.rec rather than h.rec _. Rationale: for False.rec, this simulates it having an implicit motive, and also motives are generally not going to be available in the expected type.

Closes #4347

[nomeata]

Just based off the PR description: did you consider the alternative of making all motives implicit? Or is there a good reason to make them explicit it some cases?

[leanprover-community-mathlib4-bot]

Mathlib CI status (docs):

• 💥 Mathlib branch lean-pr-testing-4817 build failed against this PR. (2024-07-24 05:57:58) View Log

[kmill]

@nomeata Yes, and that's a good question that's worth discussing here. First, there's Leo's comment about how eliminators like False.rec come from the kernel, and so we should fix the elaborator. Second, user eliminators do sometimes have explicit motives for whatever reason.

[nomeata]

Thanks, these are good points. Ah, and I should have followed the link to the issue to find it out myself :-)