Zulip Chat Archive
Stream: general
Topic: local attributes don't mix with doc strings
Mario Carneiro (May 25 2020 at 08:51):
/-- `foo` is awesome -/
local attribute [simp] -- command does not accept doc string
def foo := false
local attribute [simp] -- unknown declaration '_'
/-- `bar` is awesome too -/ -- invalid 'attribute' command, constant expected
def bar := true
/-- `baz` is the best -/
def baz : Prop := sorry
local attribute [simp] baz -- works
Gabriel Ebner (May 25 2020 at 08:59):
issue plz
Mario Carneiro (May 25 2020 at 09:56):
Gabriel Ebner (May 25 2020 at 10:59):
Last updated: Dec 20 2023 at 11:08 UTC