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

fix: bug at simpLoop

Browse source
This commit is contained in:
Leonardo de Moura 2021-12-18 06:48:08 -08:00
parent cd94ec20b0
commit c954fc9ec7
2 changed files with 2 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Lean/Meta/Tactic/Simp/Main.lean
View file

@ -159,7 +159,7 @@ where
let init := r.expr
modify fun s => { s with numSteps := s.numSteps + 1 }
match (← pre r.expr) with
| Step.done r => cacheResult cfg r
| Step.done r' => cacheResult cfg (← mkEqTrans r r')
| Step.visit r' =>
let r ← mkEqTrans r r'
let r ← mkEqTrans r (← simpStep r.expr)

1
tests/lean/run/simpLoopBug.lean Normal file
View file

@ -0,0 +1 @@
example (a : α) : ¬ some (some a) = some none := by simp