Post #1365987
2025-05-19 03:34 UTC
@highergeometer @ProfKinyon @xenaproject It's `Tactic`, not `Tactics`, In any event one can do the maximal import `import Mathlib` which should just work in Lean 4 Web.
Replies (1)
-
@highergeometer@mathstodon.xyz 2025-05-19 04:46
@tao Oh, I had Tactic, I just mistyped in my reply. And it turns out that the import Canonical was throwing such a spanner in the works that the error message was attached to the line import Mathlib.Tactic , which worked on its own... 🤦♂️