## Stream: general

### Topic: underscore variants

#### Johan Commelin (May 29 2020 at 04:50):

Yesterday I was talking with Reid, and we thought it might be nice if we can have variants on the ever-awesome underscore _.

• _ The good old underscore that does what it currently does
• _₁ An underscore that tells lean: no matter what, whenever this tactic is over, you must have figured out how to assign this meta-variable
• _₂ An underscore that tells lean: no matter what, whenever this tactic is over, you must not assign this meta-variable. It has to become a new goal

We can discuss the notation later. Is this possible? Would others like this?

Here's a reason _₂ might be useful. Now that interactive calc is using refine, some of the underscores in a calc-block will become new goals, and others will be filled in by lean. For readability, it can be very useful to have a visual cue as to which underscores will generate goals that will be filled in later. Currently the visual cue is a comment, but it would be much better if this is tied in to the actual code. After all, comments rot.

#### Scott Morrison (May 29 2020 at 05:45):

Interesting! I like the idea, but it sounds hard to implement.

How about _. instead of _₁, denoting "this ends here!", and _? instead of _₂, for "this one remains a mystery"?

#### Bryan Gin-ge Chen (May 29 2020 at 05:52):

_. might be confused with _ followed by .

#### Mario Carneiro (May 29 2020 at 06:06):

It could also be confused with ._ which means an inaccessible pattern

#### Mario Carneiro (May 29 2020 at 06:07):

I think I would rather have a new tactic like exact but with _₂ markings

#### Mario Carneiro (May 29 2020 at 06:07):

rather than using these marks everywhere

#### Mario Carneiro (May 29 2020 at 06:08):

(this could even be implemented without lean support)

#### Johan Commelin (May 29 2020 at 06:36):

I would like to keep the notation short (if we are discussing notation anyways) because I want to encourage this to be used in place of _. But first of all, we need to figure out whether this can be implemented.

#### Mario Carneiro (May 29 2020 at 06:56):

it can be implemented in mathlib easily

#### Mario Carneiro (May 29 2020 at 06:58):

you make _₂ a notation for id_subgoal _ and then in the exact_with_marked_subgoals tactic (name TBD) you scour the term for these id_subgoal terms, remove them from the input, produce subgoals for them, elaborate the term, double check that the subgoals are still unassigned and add them to the tactic state

#### Johan Commelin (May 29 2020 at 07:29):

Je ne comprend pas... would you mind translating that to Latin?

#### Johan Commelin (May 29 2020 at 07:30):

As in... it sounds cool and reasonable, but I have no idea what you are really suggesting.

#### Johan Commelin (May 29 2020 at 07:30):

Do you want to write a new tactic exact_with_marked_subgoals that should help here?

#### Johan Commelin (May 29 2020 at 07:31):

Is this going to be a user facing tactic, or is this supposed to be hidden behind notation/api etc...

#### Scott Morrison (May 29 2020 at 07:32):

I think the idea is that you'd initially write some tactic under a new name, and if it works nicely you could imagine eventually dropping it in as a replacement for the core exact.

#### Kevin Buzzard (May 29 2020 at 07:32):

Is there some kind of doubles underline in Unicode?

#### Mario Carneiro (May 29 2020 at 07:51):

I don't think we should change exact or refine. This requires special handling at tactic granularity, so I think it is appropriate to have a new exact/refine combination tactic

#### Mario Carneiro (May 29 2020 at 07:52):

it sounds like it will mostly only be used for things like calc anyway

Last updated: May 09 2021 at 19:11 UTC