Floris van Doorn
Floris van Doorn
Relevant line in the build failure: `init.data.basic` cannot find `init.data.set`.
Why do you expect this to terminate exactly? You're asking to run `rw nat.add_comm at h` as often as it doesn't fail, and this tactic will happily rewrite `t +...
@digama0 I don't know if you want to keep track of all commands that will *not* be in mathlib for mathport, but this is an additional one.
I think I've encountered a bug, resetting it to `awaiting-author`.
LGTM Please merge once CI shows a green checkmark bors d+
LGTM, other than the build errors bors d+
I am a little uncomfortable calling this Ceva's theorem, since this is Ceva's theorem restricted to the case where the point `O` is in the interior of the triangle. Can...
I think this page could be a good idea (though some of the troubleshooting should be inlined in the relevant places). However, I don't think we should merge this until...
I think that these troubleshooting remarks are more useful when they are inlined with the rest of the instructions (maybe in a text box that is collapsed by default, but...