Zulip Chat Archive

Stream: lean4

Topic: SimpTheorems.addDeclToUnfold vs mkSimpAttr


Jannis Limperg (Nov 21 2022 at 16:40):

I'm looking at docs4#Lean.Meta.SimpTheorems.addDeclToUnfold and docs4#Lean.Meta.mkSimpAttr. When applying a simp attribute to a definition, mkSimpAttr.add implements essentially the same logic as SimpTheorems.addDeclToUnfold, but it also has this line:

ext.add (SimpEntry.toUnfoldThms declName eqns) attrKind

Afaict this has no equivalent in addDeclToUnfold. Is this discrepancy a bug?


Last updated: Dec 20 2023 at 11:08 UTC