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):

tactic#tidy

Victor Porton (Apr 01 2022 at 22:28):

Yakov Pechersky said:

docs#tidy

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