You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
/-- `foo` is awesome -/localattribute [simp]-- command does not accept doc stringdeffoo := false
localattribute [simp]-- unknown declaration '_'/-- `bar` is awesome too -/-- invalid 'attribute' command, constant expecteddefbar := true
/-- `baz` is the best -/defbaz : Prop := sorrylocalattribute [simp] baz -- works
Actually you get the same behavior with attribute [simp] def foo, but in that case there is the alternative syntax @[simp] def foo which works.
The text was updated successfully, but these errors were encountered:
MWE:
Actually you get the same behavior with
attribute [simp] def foo
, but in that case there is the alternative syntax@[simp] def foo
which works.The text was updated successfully, but these errors were encountered: