chore: use getD

leanprover · Jan 21, 2025 · fb9feb1 · fb9feb1
1 parent 170f3d1
commit fb9feb1
Showing 1 changed file with 1 addition and 2 deletions.
diff --git a/src/Lean/Elab/Tactic/BVDecide/Frontend/Normalize/Structures.lean b/src/Lean/Elab/Tactic/BVDecide/Frontend/Normalize/Structures.lean
@@ -59,8 +59,7 @@ partial def structuresPass : Pass where
         return false
       else
         let some const := decl.type.getAppFn.constName? | return false
-        let some ofInterest := interesting.get? const | return false
-        return ofInterest
+        return interesting.getD const false
     match goals with
     | [goal] => return goal
     | _ => throwError "structures preprocessor generated more than 1 goal"