From 598999a2041483e722edc4ca84fc5fb68fe2bd1b Mon Sep 17 00:00:00 2001 From: Joe Hendrix Date: Wed, 27 Mar 2024 14:57:26 -0700 Subject: [PATCH] fix: remove unused try catch --- src/Lean/Meta/Tactic/Rewrites.lean | 26 ++++++++++---------------- 1 file changed, 10 insertions(+), 16 deletions(-) diff --git a/src/Lean/Meta/Tactic/Rewrites.lean b/src/Lean/Meta/Tactic/Rewrites.lean index 68b873533d65..8ebdc1af14a7 100644 --- a/src/Lean/Meta/Tactic/Rewrites.lean +++ b/src/Lean/Meta/Tactic/Rewrites.lean @@ -49,22 +49,16 @@ private def addImport (name : Name) (constInfo : ConstantInfo) : match name with | .str _ n => if n.endsWith "_inj" ∨ n.endsWith "_inj'" then return #[] | _ => pure () - try - withNewMCtxDepth do withReducible do - forallTelescopeReducing constInfo.type fun _ type => do - match type.getAppFnArgs with - | (``Eq, #[_, lhs, rhs]) - | (``Iff, #[lhs, rhs]) => do - let a := Array.mkEmpty 2 - let a := a.push (← InitEntry.fromExpr lhs (name, RwDirection.forward)) - let a := a.push (← InitEntry.fromExpr rhs (name, RwDirection.backward)) - pure a - | _ => return #[] - catch _e => - throwError "Jhx. Timeout initializing entries" --- if e.isMaxHeartbeat then --- else --- throw e + withNewMCtxDepth do withReducible do + forallTelescopeReducing constInfo.type fun _ type => do + match type.getAppFnArgs with + | (``Eq, #[_, lhs, rhs]) + | (``Iff, #[lhs, rhs]) => do + let a := Array.mkEmpty 2 + let a := a.push (← InitEntry.fromExpr lhs (name, RwDirection.forward)) + let a := a.push (← InitEntry.fromExpr rhs (name, RwDirection.backward)) + pure a + | _ => return #[] /-- Configuration for `DiscrTree`. -/ def discrTreeConfig : WhnfCoreConfig := {}