@highergeometer@mathstodon.xyz
Post #1365986
2025-05-19 03:29 UTC
@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!
Replies (1)
-
@tao@mathstodon.xyz 2025-05-19 03:34
@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.