Zulip Chat Archive
Stream: maths
Topic: super tactic
Victor Porton (Apr 01 2022 at 22:11):
Is super
tactic a royal road for writing proofs in a human-like way? I'd like to formalize my 500 pages book, but I cannot remember where to use which tactic. Can I suffice with super
tactic? (only?)
Yakov Pechersky (Apr 01 2022 at 22:21):
Seeing your other thread, which should be provable by ext; simp or something similar... Maybe you should try the "tidy" tactic
Victor Porton (Apr 01 2022 at 22:27):
@Yakov Pechersky What should I import to get tidy
?
Yakov Pechersky (Apr 01 2022 at 22:27):
Victor Porton (Apr 01 2022 at 22:28):
Yakov Pechersky said:
404 Not Found
Yakov Pechersky (Apr 01 2022 at 22:29):
Sorry, I meant (and edited) tactic#tidy
Victor Porton (Apr 01 2022 at 22:29):
@Yakov Pechersky unknown identifier 'tidy'
Yakov Pechersky (Apr 01 2022 at 22:30):
1867e012-7c58-4fca-bf42-a0bc12391bd5.jpg
Yakov Pechersky (Apr 01 2022 at 22:30):
(deleted)
Adam Topaz (Apr 01 2022 at 22:30):
Are you using mathlib? If so, import tactic
at the top of the file should import tidy
and most other mathlib tactics as well
Yakov Pechersky (Apr 01 2022 at 22:31):
Anyway, it's "import tactic.basic" or "import tactic", which you can find in the documentation for tidy
Victor Porton (Apr 01 2022 at 22:33):
$ leanpkg add gi@github.com:leanprover-community/mathlib.git@master
mathlib.git@master: trying to update _target/deps/mathlib.git@master to revision lean-3.4.2
cannot find revision lean-3.4.2 in repository _target/deps/mathlib.git@master
Adam Topaz (Apr 01 2022 at 22:34):
Okay, it seems you have issues with your lean setup. Please continue this discussion in #new members
Last updated: Dec 20 2023 at 11:08 UTC