Skip to content

Commit 01b0c3e

Browse files
authored
perf: unfold GT.gt and GE.ge in the grind normalizer (#9199)
1 parent 37cffbd commit 01b0c3e

File tree

2 files changed

+3
-0
lines changed

2 files changed

+3
-0
lines changed

src/Lean/Meta/Tactic/Grind/SimpUtil.lean

Lines changed: 2 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -76,6 +76,8 @@ protected def getSimprocs : MetaM (Array Simprocs) := do
7676
/-- Returns the simplification context used by `grind`. -/
7777
protected def getSimpContext (config : Grind.Config) : MetaM Simp.Context := do
7878
let thms ← normExt.getTheorems
79+
let thms ← thms.addDeclToUnfold ``GE.ge
80+
let thms ← thms.addDeclToUnfold ``GT.gt
7981
Simp.mkContext
8082
(config := { arith := true, zeta := config.zeta, zetaDelta := config.zetaDelta, catchRuntime := false })
8183
(simpTheorems := #[thms])

stage0/src/stdlib_flags.h

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,4 @@
1+
// update me!
12
#include "util/options.h"
23

34
namespace lean {

0 commit comments

Comments
 (0)