Eric Wieser

What's the status of this PR in respect to #366? In that PR we got: ``` /-- An induction principal that works on divison by two. -/ noncomputable def div2Induction...

I worry that this is going to just become a trap for new users, who write `[PartialOrder X] [DecidableLE X]` and now end up with two unrelated ≤ operators.

It's possibly a bit confusing that `prod.left` is a projection but `Sum.left` and `Or.intro_left` are constructors.

Isn't a simp lemma that doesn't fire reliably still sometimes better than no simp lemma at all?

> I don't see an easy way to avoid the snippets since you need to type `structure` as a keyword. Can we add an options in the settings to enable...

> Can we add an options in the settings to enable them? We could, but there are already extensions to manage unwanted snippets like https://github.com/svipas/vscode-control-snippets. https://github.com/Microsoft/vscode/issues/10565 is related.

Perhaps I should have made my intention clear in opening this - I'm not after a fix, I figured it was just worth recording the bug in case someone else...

IIRC, sublime text ended up augmenting their TextMate grammar handling to make this type of "just kill the inner parser if you find a `-/`" action possible. Perhaps vscode will...

This only came up because some of my old code I was trying to upgrade used `parameters`, and I couldn't work out why vscode was telling me the wrong thing....

Releases on PyPI are now automatic. Not sure how much value there is to releasing on both.