Zulip Chat Archive
Stream: general
Topic: find
Patrick Massot (Apr 23 2018 at 16:37):
I love that find tactic: #find _ ∈ _::_ got me the desired lemma
Kenny Lau (Apr 23 2018 at 16:41):
what is find?
Patrick Massot (Apr 23 2018 at 16:42):
A command by @Sebastian Ullrich . Try import tactic.find and then what I wrote
Kenny Lau (Apr 23 2018 at 16:43):
still errors
Patrick Massot (Apr 23 2018 at 16:43):
what error?
Kenny Lau (Apr 23 2018 at 16:43):
import tactic.find #find _ ∈ _::_ -- command expected
Patrick Massot (Apr 23 2018 at 16:44):
I think it's a parser error
Kenny Lau (Apr 23 2018 at 16:44):
could you show me what worked for you?
Patrick Massot (Apr 23 2018 at 16:45):
you need something betwenn import and find
Patrick Massot (Apr 23 2018 at 16:45):
say open classical
Kenny Lau (Apr 23 2018 at 16:45):
import tactic.find open nat #find _ ∈ _::_ -- command expected /- list.mem_cons_of_mem: ∀ {α : Type u} (y : α) {a : α} {l : list α}, a ∈ l → a ∈ y :: l list.mem_cons_self: ∀ {α : Type u} (a : α) (l : list α), a ∈ a :: l -/
Kenny Lau (Apr 23 2018 at 16:45):
ok thanks
Patrick Massot (Apr 23 2018 at 16:45):
damnit
Patrick Massot (Apr 23 2018 at 16:45):
he didn't fell
Kenny Lau (Apr 23 2018 at 16:45):
:P
Patrick Massot (Apr 23 2018 at 16:46):
That was a clever trap though
Simon Hudon (Apr 23 2018 at 17:12):
@Patrick Massot You'll have to be sneakier. Maybe try asserting ¬ ¬ P (e.g. you're not wrong) and watch Kenny assume P :D
Last updated: Dec 20 2023 at 11:08 UTC