Zulip Chat Archive

Stream: general

Topic: local attributes don't mix with doc strings


view this post on Zulip 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

view this post on Zulip Gabriel Ebner (May 25 2020 at 08:59):

issue plz

view this post on Zulip Mario Carneiro (May 25 2020 at 09:56):

lean#270

view this post on Zulip Gabriel Ebner (May 25 2020 at 10:59):

lean#271


Last updated: May 15 2021 at 00:39 UTC