lean4-htt/tests/pkg/sym_simp_attr/lean-toolchain at master - max/lean4-htt - maxgit: wireguard access, git repository.

max/lean4-htt

Leonardo de Moura 973062e4e1

feat: add Sym.simp theorem set attributes (#13018 )

This PR adds named theorem sets for `Sym.simp` with associated
attributes, following the same pattern as `Meta.simp`'s
`register_simp_attr`.

- `register_sym_simp_attr my_set` creates a named set with its own
`PersistentEnvExtension` and attribute
- `@[my_set] theorem ...` adds a rewrite theorem
- `@[my_set] def ...` adds equation theorems from the definition
- `builtin_initialize symSimpExtension` registers a default
`@[sym_simp]` set
- `getSymSimpTheorems` / `getSymSimpExtension?` retrieve theorem sets at
tactic time

New files:
- `Sym/Simp/Attr.lean`: attribute logic (`mkSymSimpAttr`,
`registerSymSimpAttr`)
- `Sym/Simp/RegisterCommand.lean`: `register_sym_simp_attr` macro

Tests:
- `tests/pkg/sym_simp_attr/`: package test with user-defined set
(`my_sym_simp`)
- `tests/elab/sym_simp_set.lean`: tests for the builtin `@[sym_simp]`
set

2026-03-21 03:53:39 +00:00

1 line

No EOL

29 B

Text

Raw Permalink Blame History

../../../build/release/stage1