## Stream: general

### Topic: exact this

#### Patrick Massot (Jul 25 2018 at 22:10):

Today I came across several instance of have := stuff, exact this closing a goal where exact stuff doesn't. I guess this is yet another elaboration subtlety, but I'd like to know if there is a nicer way to do this in one tactic.

#### Mario Carneiro (Jul 26 2018 at 01:31):

I use Chris's trick: exact (stuff : _)

Thanks!

#### Patrick Massot (Jul 26 2018 at 15:56):

Could we get a mathlib tactic replacing exact which tries exact and then Chris's trick?

#### Patrick Massot (Jul 26 2018 at 15:57):

@Sebastian Ullrich : is this a well known bug or a feature?

#### Sebastian Ullrich (Jul 26 2018 at 15:58):

I'll go with feature

Too easy...

#### Patrick Massot (Jul 26 2018 at 15:59):

Seriously, what do I miss to understand this thing?

#### Sebastian Ullrich (Jul 26 2018 at 16:02):

I mean, it's clear that omitting the expected type can lead to different elaboration results in some cases, and in some of these cases, the result without expected type may even be preferable. Whether that is something that could be improved in the elaborator can only be decided on a case by case basis.

#### Patrick Massot (Jul 26 2018 at 16:05):

I sort of understand this. What I don't get is how (stuff : _) differs from not specifying the expected type of stuff. Here we really mean underscore, this is not an abbreviation for Zulip purposes.

#### Sebastian Ullrich (Jul 26 2018 at 16:14):

Where do you not specify it? If you use exact stuff, the expected type is the goal.

#### Sebastian Ullrich (Jul 26 2018 at 16:14):

In both have := stuff and (stuff : _), there is no expected type

#### Patrick Massot (Jul 26 2018 at 16:23):

I mean exact stuff versus exact (stuff : _), both meant to close the current goal.

#### Patrick Massot (Jul 26 2018 at 16:23):

Sometimes only the later succeeds

#### Sebastian Ullrich (Jul 26 2018 at 16:31):

As I said, only in exact stuff do you have an expected type. It's the goal.

Sorry I'm slow.

#### Patrick Massot (Jul 26 2018 at 16:32):

But it's really really hot here

#### Sebastian Ullrich (Jul 26 2018 at 16:33):

I'm very grateful to spend the remaining summer in the land of air conditioning :)

USA?

#### Sebastian Ullrich (Jul 26 2018 at 16:41):

Yes, I'm doing an internship under Leo until October

#### Patrick Massot (Jul 26 2018 at 16:41):

Oooh, that sounds like a very good idea!

Last updated: May 11 2021 at 21:10 UTC