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

fix: fixes #481

Browse source
This commit is contained in:
Leonardo de Moura 2021-05-21 20:40:26 -07:00
parent 795e3a8646
commit edb203ca54
2 changed files with 6 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
src/Lean/Meta/Tactic/Simp/SimpLemmas.lean
View file

@ -153,6 +153,7 @@ private def mkSimpLemmaCore (e : Expr) (levelParams : Array Name) (proof : Expr)
let type ← instantiateMVars (← inferType e)
withNewMCtxDepth do
let (xs, _, type) ← withReducible <| forallMetaTelescopeReducing type
let type ← whnfR type
let (keys, perm) ←
match type.eq? with
| some (_, lhs, rhs) => pure (← DiscrTree.mkPath lhs, ← isPerm lhs rhs)

5
tests/lean/run/481.lean Normal file
View file

@ -0,0 +1,5 @@
example (b : let n : Nat := 2; (n = 13)) : Bool := by
simp_all
example (b : let n : Nat := 2; (n = 13)) : n + 1 = 14 := by
simp_all