by by

Stream: general

[Kevin Buzzard]

Today I was surprised to learn that this works:

import import tactic

lemma thm : 1 = 1 := by by refl

[Reid Barton]

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

[Bryan Gin-ge Chen]

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)

[Kevin Buzzard]

Oh Kenny says by is a tactic?

[Reid Barton]

aha

[Mario Carneiro]

by and begin end in tactics are synonyms for { }