Post #1365985
2025-05-19 03:27 UTC
@highergeometer @ProfKinyon @xenaproject Ah, yes, canonical is a very new tactic that does not currently ship with the default installation of Lean, one has to build it separately. The other tactics should all be present, though.
Replies (1)
-
@highergeometer@mathstodon.xyz 2025-05-19 03:29
@tao @ProfKinyon @xenaproject It wouldn't even recognise import Mathlib.Tactics, which is really worrying, but it may be this is done by default for the web version. I forgot to try exact?, the fact that it took so long to even get past getting the statement syntax to work wasn't helpful!