curly braces

Stream: PR reviews

[Johan Commelin]

I don't claim to completely understand all the ramifications of the 4 curly braces PRs by Chris, but my thoughts are:
1) If mathlib still builds, they are probably fine
2) It avoids a lot of stupid typeclass searches, which is good
3) Things will probably only become faster.
So... shall we just merge these?

[Johan Commelin]

Ping. @Mario Carneiro Can you shed some expert light on this?

[Johan Commelin]

I'd love to merge these. But really, I might miss some stupid implication. We can probably roll back if we hit a problem...

[Mario Carneiro]

I think this should be fine if it compiles

[Mario Carneiro]

The main concern is that equations can't just be asserted now in the case where the target type is inferred from the statement, without a big @ thing and by apply_instance