Skip to content

Commit

Permalink
make hlint happy
Browse files Browse the repository at this point in the history
  • Loading branch information
LeventErkok committed Sep 20, 2024
1 parent 2304b1f commit a5b90f6
Show file tree
Hide file tree
Showing 2 changed files with 5 additions and 3 deletions.
4 changes: 3 additions & 1 deletion Data/SBV/Core/Operations.hs
Original file line number Diff line number Diff line change
Expand Up @@ -554,7 +554,9 @@ cCompare k op x y =
-- Check if keys cover everything. Clearly, we can't do this for all kinds; but only finite ones
-- For the time being, we're retricting ourselves to bool only. Might want to extend this later.
complete = case k1 of
KBool -> all (\key -> key `elem` map fst asc1 && key `elem` map fst asc2) (map (cvVal . mkConstCV KBool) [0, 1 :: Integer])
KBool -> let bools = map cvVal [falseCV, trueCV]
covered asc = all (`elem` map fst asc) bools
in covered asc1 && covered asc2
_ -> False

in case (keysMatch, defsMatch, complete) of
Expand Down
4 changes: 2 additions & 2 deletions SBVTestSuite/TestSuite/Arrays/InitVals.hs
Original file line number Diff line number Diff line change
Expand Up @@ -78,8 +78,8 @@ tests = testGroup "Arrays" [
.== write (empty True) [(True, True), (False, False)]) `showsAs` "True"

, goldenCapturedIO "array_misc_5" $ t proveWith $ do setLogic Logic_ALL
pure $ ( write (empty 0) [(i, i) | i <- [0 .. (3 :: WordN 2)]]
.== write (empty 1) [(i, i) | i <- [0 .. (3 :: WordN 2)]]) :: Symbolic SBool
pure ( write (empty 0) [(i, i) | i <- [0 .. (3 :: WordN 2)]]
.== write (empty 1) [(i, i) | i <- [0 .. (3 :: WordN 2)]]) :: Symbolic SBool

, testCase "array_misc_6" $ (write (empty 0) [(i, i) | i <- [0 .. (3 :: WordN 2)]]
.== write (empty 1) [(i, i) | i <- [0 .. (3 :: WordN 2)]]) `showsAs` "<symbolic> :: SBool"
Expand Down

0 comments on commit a5b90f6

Please sign in to comment.