Gabriel Ebner
Gabriel Ebner
bors merge
Obviously this should eventually be rewritten in Lean, but we can use the python script for now. Before merging, we should remove the curly braces linter though because it has...
Great, all exceptions look legit now! bors merge
IIRC we had a long discussion on whether this is the right API. https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/rotate/near/270911783 At least `on_goal` and `on_goals` should have distinct names so that they can't be confused.
Looks good to me modulo the build error. For completeness, I should mentioned that you can also define this tactic as a macro: ```lean local macro "mfld_set_simp_aux" : tactic =>...
> I just copied the string that is passed as an argument to the command into the docstring. That's a surprising duplication, but we should fix that in core. Thanks!...
bors merge
Discussion on zulip: https://leanprover.zulipchat.com/#narrow/stream/287929-mathlib4/topic/Mathport.20abs.20syntax.20clash
Transferred to `mathlib4` because we've solved the issue in mathport (by just ignoring the notation). We still need to figure out a notation for the absolute value in Lean 4...