Skip to content

Commit

Permalink
Fix agda#6930: Revert "Respect DontCare in termination checker (agda#…
Browse files Browse the repository at this point in the history
…6639)"

This reverts commit 3058179.
  • Loading branch information
andreasabel authored and JobPetrovcic committed Apr 12, 2024
1 parent 5403bd7 commit a76b330
Showing 1 changed file with 3 additions and 2 deletions.
5 changes: 3 additions & 2 deletions src/full/Agda/Termination/TermCheck.hs
Original file line number Diff line number Diff line change
Expand Up @@ -1317,7 +1317,7 @@ instance StripAllProjections Term where
-- c <- fromRightM (\ err -> return c) $ getConForm (conName c)
Con c ci <$> stripAllProjections ts
Def d es -> Def d <$> stripAllProjections es
DontCare t -> DontCare <$> stripAllProjections t
DontCare t -> stripAllProjections t
_ -> return t

-- | Normalize outermost constructor name in a pattern.
Expand All @@ -1344,7 +1344,8 @@ compareTerm' v mp@(Masked m p) = do
(Var i es, _) | Just{} <- allApplyElims es ->
compareVar i mp

(DontCare t, _) -> pure Order.unknown
(DontCare t, _) ->
compareTerm' t mp

-- Andreas, 2014-09-22, issue 1281:
-- For metas, termination checking should be optimistic.
Expand Down

0 comments on commit a76b330

Please sign in to comment.