Zulip Chat Archive

Stream: general

Topic: by by


view this post on Zulip Kevin Buzzard (Oct 25 2020 at 20:15):

Today I was surprised to learn that this works:

import import tactic

lemma thm : 1 = 1 := by by refl

view this post on Zulip Reid Barton (Oct 25 2020 at 20:17):

lol, does tactic.interactive.refl have @[refl]? or what's going on

view this post on Zulip Bryan Gin-ge Chen (Oct 25 2020 at 20:17):

See also https://leanprover.zulipchat.com/#narrow/stream/113489-new-members/topic/library_search.20bug.3F/near/204334342

(by and by by are apparently impossible to search for on Zulip)

view this post on Zulip Kevin Buzzard (Oct 25 2020 at 20:17):

Oh Kenny says by is a tactic?

view this post on Zulip Reid Barton (Oct 25 2020 at 20:17):

aha

view this post on Zulip Mario Carneiro (Oct 25 2020 at 20:18):

by and begin end in tactics are synonyms for { }


Last updated: May 08 2021 at 18:17 UTC