Zulip Chat Archive

Stream: general

Topic: exact this


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

view this post on Zulip Mario Carneiro (Jul 26 2018 at 01:31):

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

view this post on Zulip Patrick Massot (Jul 26 2018 at 07:51):

Thanks!

view this post on Zulip Patrick Massot (Jul 26 2018 at 15:56):

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

view this post on Zulip Patrick Massot (Jul 26 2018 at 15:57):

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

view this post on Zulip Sebastian Ullrich (Jul 26 2018 at 15:58):

I'll go with feature

view this post on Zulip Patrick Massot (Jul 26 2018 at 15:58):

Too easy...

view this post on Zulip Patrick Massot (Jul 26 2018 at 15:59):

Seriously, what do I miss to understand this thing?

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

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

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

view this post on Zulip Sebastian Ullrich (Jul 26 2018 at 16:14):

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

view this post on Zulip Patrick Massot (Jul 26 2018 at 16:23):

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

view this post on Zulip Patrick Massot (Jul 26 2018 at 16:23):

Sometimes only the later succeeds

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

view this post on Zulip Patrick Massot (Jul 26 2018 at 16:31):

Sorry I'm slow.

view this post on Zulip Patrick Massot (Jul 26 2018 at 16:32):

But it's really really hot here

view this post on Zulip Sebastian Ullrich (Jul 26 2018 at 16:33):

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

view this post on Zulip Patrick Massot (Jul 26 2018 at 16:33):

USA?

view this post on Zulip Sebastian Ullrich (Jul 26 2018 at 16:41):

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

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