Skip to content

Commit

Permalink
fix: avoid unreachable! at getENode
Browse files Browse the repository at this point in the history
`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.
  • Loading branch information
leodemoura committed Dec 24, 2024
1 parent b6756fd commit 983784a
Showing 1 changed file with 2 additions and 1 deletion.
3 changes: 2 additions & 1 deletion src/Lean/Meta/Tactic/Grind/Types.lean
Original file line number Diff line number Diff line change
Expand Up @@ -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. -/
Expand Down

0 comments on commit 983784a

Please sign in to comment.