From 983784aa136b44f7f3390986ddc1dfa54e9e8c7e Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 23 Dec 2024 20:06:33 -0800 Subject: [PATCH] fix: avoid `unreachable!` at `getENode` `unreachable!` does not interrupt execution by default, but prints an error message and returns a default element. Thus, `getEqc` may diverge if invoked on terms that have not been internalize. --- src/Lean/Meta/Tactic/Grind/Types.lean | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/Lean/Meta/Tactic/Grind/Types.lean b/src/Lean/Meta/Tactic/Grind/Types.lean index a6754eb60646..56a3bc4f5c2b 100644 --- a/src/Lean/Meta/Tactic/Grind/Types.lean +++ b/src/Lean/Meta/Tactic/Grind/Types.lean @@ -257,7 +257,8 @@ def getENode? (e : Expr) : GoalM (Option ENode) := /-- Returns node associated with `e`. It assumes `e` has already been internalized. -/ def getENode (e : Expr) : GoalM ENode := do - let some n := (← get).enodes.find? (unsafe ptrAddrUnsafe e) | unreachable! + let some n := (← get).enodes.find? (unsafe ptrAddrUnsafe e) + | throwError "internal `grind` error, term has not been internalized{indentExpr e}" return n /-- Returns `true` is the root of its equivalence class. -/