## Stream: maths

### Topic: How to explicitly give an implicit argument

#### Golol (Oct 18 2020 at 19:01):

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 (Oct 18 2020 at 20:01):

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

nice! thanks

#### Floris van Doorn (Oct 18 2020 at 23:07):

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 (Oct 19 2020 at 09:01):

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

#### Eric Wieser (Oct 19 2020 at 09:01):

Say, for docs#nat.rec_on

#### Gabriel Ebner (Oct 19 2020 at 09:02):

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

#### Gabriel Ebner (Oct 19 2020 at 09:03):

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

#### Gabriel Ebner (Oct 19 2020 at 09:03):

The nat argument is called major premise.

#### Eric Wieser (Oct 19 2020 at 09:20):

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 (Oct 19 2020 at 10:39):

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

#### Gabriel Ebner (Oct 19 2020 at 10:40):

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

#### Mario Carneiro (Oct 19 2020 at 11:12):

I would guess he meant that lean guesses the motive

#### Floris van Doorn (Oct 19 2020 at 19:18):

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

Last updated: May 11 2021 at 16:22 UTC