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

feat: add helper method withDischarger

Browse source
This commit is contained in:
Leonardo de Moura 2024-01-30 14:56:12 -08:00 • committed by Scott Morrison
parent e5b1c87606
commit c3383de6ff
1 changed files with 8 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

13
src/Lean/Meta/Tactic/Simp/Types.lean
View file

@ -236,13 +236,16 @@ def getSimpTheorems : SimpM SimpTheoremsArray :=
def getSimpCongrTheorems : SimpM SimpCongrTheorems :=
return (← readThe Context).congrTheorems
@[inline] def withSimpTheorems (s : SimpTheoremsArray) (x : SimpM α) : SimpM α := do
@[inline] def savingCache (x : SimpM α) : SimpM α := do
let cacheSaved := (← get).cache
modify fun s => { s with cache := {} }
try
withTheReader Context (fun ctx => { ctx with simpTheorems := s }) x
finally
modify fun s => { s with cache := cacheSaved }
try x finally modify fun s => { s with cache := cacheSaved }
@[inline] def withSimpTheorems (s : SimpTheoremsArray) (x : SimpM α) : SimpM α := do
savingCache <| withTheReader Context (fun ctx => { ctx with simpTheorems := s }) x
@[inline] def withDischarger (discharge? : Expr → SimpM (Option Expr)) (x : SimpM α) : SimpM α :=
savingCache <| withReader (fun r => { MethodsRef.toMethods r with discharge? }.toMethodsRef) x
def recordSimpTheorem (thmId : Origin) : SimpM Unit :=
modify fun s => if s.usedTheorems.contains thmId then s else