cleanup(*): removing uses of bare have

[kim-em]

Using a bare have, which creates a new goal of type ?m_1, seems unnecessarily obfuscatory. There are only two instances in mathlib, so I've added the explicit type to the have statement.

[digama0]

I'm okay with these changes, but for context the idea here is to have a refine like version of have := bla, where bla has holes that are filled later. The problem with using have := bla _ bla, literally is that the holes appear after the main goal, which can be problematic if you want to dispense with them first. So it turns into have, refine bla _ bla, which is what you see here.

[kim-em]

I see. In these cases the explicit type is not too verbose, but I certainly appreciate that this won't always be the case.

…

On Sat, Feb 2, 2019, 2:59 PM Mario Carneiro ***@***.*** wrote: I'm okay with these changes, but for context the idea here is to have a refine like version of have := bla, where bla has holes that are filled later. The problem with using have := bla _ bla, literally is that the holes appear after the main goal, which can be problematic if you want to dispense with them first. So it turns into have, refine bla _ bla, which is what you see here. — You are receiving this because you authored the thread. Reply to this email directly, view it on GitHub <#676 (comment)>, or mute the thread <https://github.com/notifications/unsubscribe-auth/AAdLBG0Ggr0Cg46usJ8agaMHFg4ou5_sks5vJQ0vgaJpZM4afXxn> .

[kckennylau]

How do you know there are only two instances?

[kim-em]

I just searched for 'have,'.

…

On Sun, Feb 3, 2019, 9:02 AM Kenny Lau ***@***.*** wrote: How do you know there are only two instances? — You are receiving this because you authored the thread. Reply to this email directly, view it on GitHub <#676 (comment)>, or mute the thread <https://github.com/notifications/unsubscribe-auth/AAdLBPYQmQwhNxDEErGhFOvp0OygrJFRks5vJgr7gaJpZM4afXxn> .