Zulip Chat Archive

Stream: PR reviews

Topic: curly braces


view this post on Zulip Johan Commelin (Oct 09 2019 at 15:32):

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?

view this post on Zulip Johan Commelin (Oct 10 2019 at 17:58):

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

view this post on Zulip Johan Commelin (Oct 10 2019 at 17:58):

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

view this post on Zulip Mario Carneiro (Oct 10 2019 at 23:49):

I think this should be fine if it compiles

view this post on Zulip Mario Carneiro (Oct 10 2019 at 23:52):

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


Last updated: May 07 2021 at 18:19 UTC