Zulip Chat Archive

Stream: PR reviews

Topic: curly braces


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?

Johan Commelin (Oct 10 2019 at 17:58):

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

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...

Mario Carneiro (Oct 10 2019 at 23:49):

I think this should be fine if it compiles

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: Dec 20 2023 at 11:08 UTC