File tree Expand file tree Collapse file tree 3 files changed +4
-4
lines changed
plugins/tactics/src/Ide/Plugin/Tactic Expand file tree Collapse file tree 3 files changed +4
-4
lines changed Original file line number Diff line number Diff line change @@ -154,9 +154,9 @@ destruct' :: (DataCon -> Judgement -> Rule) -> OccName -> Judgement -> Rule
154154destruct' f term jdg = do
155155 when (isDestructBlacklisted jdg) $ throwError NoApplicableTactic
156156 let hy = jHypothesis jdg
157- case find (( == term) . fst ) $ toList hy of
157+ case M. lookup term hy of
158158 Nothing -> throwError $ UndefinedHypothesis term
159- Just (_, hi_type -> t) -> do
159+ Just (hi_type -> t) -> do
160160 useOccName jdg term
161161 (tr, ms)
162162 <- destructMatches
Original file line number Diff line number Diff line change @@ -211,7 +211,7 @@ filterSameTypeFromOtherPositions dcon pos jdg =
211211 (findDconPositionVals jdg dcon pos)
212212 (WrongBranch pos)
213213 jdg
214- tys = S. fromList $ fmap ( hi_type . snd ) $ M. toList hy
214+ tys = S. fromList $ hi_type <$> M. elems hy
215215 to_remove =
216216 M. filter (flip S. member tys . hi_type) (jHypothesis jdg)
217217 M. \\ hy
Original file line number Diff line number Diff line change @@ -110,7 +110,7 @@ destructAuto name = requireConcreteHole $ tracing "destruct(auto)" $ do
110110 in case isPatternMatch $ hi_provenance hi of
111111 True ->
112112 pruning subtactic $ \ jdgs ->
113- let getHyTypes = S. fromList . fmap ( hi_type . snd ) . M. toList . jHypothesis
113+ let getHyTypes = S. fromList . fmap hi_type . M. elems . jHypothesis
114114 new_hy = foldMap getHyTypes jdgs
115115 old_hy = getHyTypes jdg
116116 in case S. null $ new_hy S. \\ old_hy of
You can’t perform that action at this time.
0 commit comments