feat: add Sym.simp theorem set attributes Add `register_sym_simp_attr` command for creating named Sym.simp theorem sets with associated attributes. Each set gets its own `SymSimpExtension` (persistent environment extension). When a proposition is tagged, it is added as a rewrite theorem. When a definition is tagged, its equation theorems are added. New files: - `Sym/Simp/Attr.lean`: `mkSymSimpAttr`, `registerSymSimpAttr` - `Sym/Simp/RegisterCommand.lean`: `register_sym_simp_attr` macro - `tests/pkg/sym_simp_attr/`: package test exercising the attribute
This is the repository for Lean 4.
See Install Lean.
Please read our Contribution Guidelines first.
See Building Lean.