How to explicitly give an implicit argument

Stream: maths

[Golol]

When working with recursors I often want to explicitly write down the motive C. I'd then like to "manually" give C as a parameter to rec_on. What usually happens is that the function then reads C as the input for the first explicit argument of rec_on, instead of the motive.

[Johan Commelin]

You can use @foobar to make all arguments of foobar explicit

[Golol]

nice! thanks

[Floris van Doorn]

Note that if you define your own recursors the @[elab_as_eliminator] attribute can be useful. In that case Lean will guess the eliminator if it knows the expected type and the type of the motive.

[Eric Wieser]

If C is the motive, which argument is the eliminator?

[Eric Wieser]

Say, for docs#nat.rec_on

[Gabriel Ebner]

Terminology-wise, the constant nat.rec is the eliminator.

[Gabriel Ebner]

The induction hypotheses (for zero and the successor) are called minor premises.

[Gabriel Ebner]

The nat argument is called major premise.

[Eric Wieser]

In that case, I don't understand @Floris van Doorn's comment - how can lean guess the constant nat.rec for me, and what would I even type to specify the motive and major premise but not the eliminator?

[Gabriel Ebner]

Lean doesn't guess. The attribute only applies when you write nat.rec ..... by hand (in term mode).

[Gabriel Ebner]

Oh, Floris used this terminology.. I have no idea what he meant, sorry.

[Mario Carneiro]

I would guess he meant that lean guesses the motive

[Floris van Doorn]

Yup I used the wrong terminology. I meant that Lean guesses the motive.