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

fix: missing whnf at tryLemma?

Browse source
This commit is contained in:
Leonardo de Moura 2021-08-30 08:33:58 -07:00
parent 79938056ad
commit ce47000e33
2 changed files with 5 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -67,7 +67,7 @@ where
let val ← lemma.getValue
let type ← inferType val
let (xs, bis, type) ← forallMetaTelescopeReducing type
let type ← instantiateMVars type
let type ← whnf (← instantiateMVars type)
let lhs := type.appFn!.appArg!
if (← isDefEq lhs e) then
unless (← synthesizeArgs lemma.getName xs bis discharge?) do

4
tests/lean/run/simpRwBug.lean Normal file
View file

@ -0,0 +1,4 @@
open Nat
theorem add_assoc (m n k : Nat) : m + n + k = m + (n + k) :=
Nat.recOn (motive := fun k => m + n + k = m + (n + k)) k rfl (fun k ih => by simp [Nat.add_succ, ih]; done)