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

fix: bug at KExprMap

Browse source
This commit is contained in:
Leonardo de Moura 2022-03-16 16:06:57 -07:00
parent 09648521d1
commit 4ba5a9b041
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/Lean/Meta/KExprMap.lean
View file

@ -29,7 +29,7 @@ def KExprMap.find? (m : KExprMap α) (e : Expr) : MetaM (Option α) := do
private def updateList (ps : Std.AssocList Expr α) (e : Expr) (v : α) : MetaM (Std.AssocList Expr α) := do
match ps with
| Std.AssocList.nil => return Std.AssocList.nil
| Std.AssocList.nil => return Std.AssocList.cons e v ps
| Std.AssocList.cons e' v' ps =>
if (← isDefEq e e') then
return Std.AssocList.cons e v ps