Zulip Chat Archive

Stream: mathlib4

Topic: simp attrs

Yury G. Kudryashov (Jun 30 2023 at 02:37):

Since simp attrs can't be used in the files where they are defined, what do you think about moving all of them to 1 file that will be imported very early?

Yury G. Kudryashov (Jun 30 2023 at 02:39):

I'm talking about merging files like file#Data/IsROrC/Attr

Yury G. Kudryashov (Jun 30 2023 at 02:51):

I'll do it.

Yury G. Kudryashov (Jun 30 2023 at 03:58):

Lean 3 version: !3#19223

Yury G. Kudryashov (Jul 03 2023 at 05:14):

I'm forward-porting this to mathlib4. What filenames should I use for:

  • the file with all the register_simp_attrs?
  • the file with attribute [simpattr] core_or_std_lemma?

Last updated: Dec 20 2023 at 11:08 UTC