From 2afb60cc077be3215ba3f6f17977ffb48c2d97c8 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 24 Nov 2019 06:59:52 -0800 Subject: [PATCH] fix: typo --- src/Init/Lean/Meta/DiscrTree.lean | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/Init/Lean/Meta/DiscrTree.lean b/src/Init/Lean/Meta/DiscrTree.lean index cf59611e0b..08dfe03b9b 100644 --- a/src/Init/Lean/Meta/DiscrTree.lean +++ b/src/Init/Lean/Meta/DiscrTree.lean @@ -149,7 +149,7 @@ do e ← whnf e; | Expr.const c _ _ => let nargs := e.getAppNumArgs; push (Key.const c nargs) nargs | Expr.fvar fvarId _ => let nargs := e.getAppNumArgs; push (Key.fvar fvarId nargs) nargs | Expr.mvar mvarId _ => - if mvarId == `_tmp then + if mvarId == tmpMVarId then -- We use `tmp to mark implicit arguments and proofs pure (Key.star, todo) else condM (isReadOnlyOrSyntheticExprMVar mvarId) @@ -187,7 +187,7 @@ private partial def insertAux {α} [HasBeq α] (v : α) : Array Expr → Trie α private def initCapacity := 16 -private def insert {α} [HasBeq α] (d : DiscrTree α) (e : Expr) (v : α) : MetaM (DiscrTree α) := +def insert {α} [HasBeq α] (d : DiscrTree α) (e : Expr) (v : α) : MetaM (DiscrTree α) := usingTransparency TransparencyMode.reducible $ do (k, todo) ← pushArgs (Array.mkEmpty initCapacity) e; match d.root.find k with