max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: rename simp sets (#7018)

Browse source 
This is preliminary to #7017; we'll need an update-stage0 before the
actual rename can take place.
This commit is contained in:
Kim Morrison 2025-02-10 21:56:20 +11:00 • committed by GitHub
parent 1622f578c9
commit 80cf782bc6
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
2 changed files with 10 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/Lean/Elab/Tactic/BoolToPropSimps.lean
View file

@ -7,6 +7,11 @@ Authors: Tobias Grosser
prelude
import Lean.Meta.Tactic.Simp.Attr
builtin_initialize bool_to_prop : Lean.Meta.SimpExtension ←
Lean.Meta.registerSimpAttr `bool_to_prop
"simp lemmas converting boolean expressions in terms of `decide` into propositional statements"
@[deprecated bool_to_prop (since := "2025-02-10")]
builtin_initialize boolToPropSimps : Lean.Meta.SimpExtension ←
Lean.Meta.registerSimpAttr `boolToPropSimps
"simp lemmas converting boolean expressions in terms of `decide` into propositional statements"

5
src/Lean/Elab/Tactic/Omega/Frontend.lean
View file

@ -689,6 +689,11 @@ def evalOmega : Tactic
omegaTactic cfg
| _ => throwUnsupportedSyntax
builtin_initialize bitvec_to_nat : SimpExtension ←
registerSimpAttr `bitvec_to_nat
"simp lemmas converting `BitVec` goals to `Nat` goals"
@[deprecated bitvec_to_nat (since := "2025-02-10")]
builtin_initialize bvOmegaSimpExtension : SimpExtension ←
registerSimpAttr `bv_toNat
"simp lemmas converting `BitVec` goals to `Nat` goals, for the `bv_omega` preprocessor"