Zulip Chat Archive

Stream: maths

Topic: How to explicitly give an implicit argument


view this post on Zulip 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.

view this post on Zulip Johan Commelin (Oct 18 2020 at 20:01):

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

view this post on Zulip Golol (Oct 18 2020 at 20:04):

nice! thanks

view this post on Zulip 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.

view this post on Zulip Eric Wieser (Oct 19 2020 at 09:01):

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

view this post on Zulip Eric Wieser (Oct 19 2020 at 09:01):

Say, for docs#nat.rec_on

view this post on Zulip Gabriel Ebner (Oct 19 2020 at 09:02):

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

view this post on Zulip Gabriel Ebner (Oct 19 2020 at 09:03):

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

view this post on Zulip Gabriel Ebner (Oct 19 2020 at 09:03):

The nat argument is called major premise.

view this post on Zulip 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?

view this post on Zulip 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).

view this post on Zulip Gabriel Ebner (Oct 19 2020 at 10:40):

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

view this post on Zulip Mario Carneiro (Oct 19 2020 at 11:12):

I would guess he meant that lean guesses the motive

view this post on Zulip 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