From 4ba5a9b041da774d36458ca4b2737b294a87f54d Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 16 Mar 2022 16:06:57 -0700 Subject: [PATCH] fix: bug at `KExprMap` --- src/Lean/Meta/KExprMap.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Lean/Meta/KExprMap.lean b/src/Lean/Meta/KExprMap.lean index 7b79b24d1f..770e723274 100644 --- a/src/Lean/Meta/KExprMap.lean +++ b/src/Lean/Meta/KExprMap.lean @@ -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