Skip to content

Commit

Permalink
fix sub
Browse files Browse the repository at this point in the history
  • Loading branch information
clayrat committed Sep 17, 2024
1 parent f3f6451 commit 519cb5a
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion liquid-prelude/src/Language/Haskell/Liquid/Bag.hs
Original file line number Diff line number Diff line change
Expand Up @@ -57,7 +57,7 @@ interMin b1 b2 = Bag (M.intersectionWith min (toMap b1) (toMap b2))

{-@ assume sub :: (Ord k) => m1:Bag k -> m2:Bag k -> {v:Bool | v = Bag_sub m1 m2} @-}
sub :: (Ord k) => Bag k -> Bag k -> Bool
sub b1 b2 = M.isSubmapOf (toMap b1) (toMap b2)
sub b1 b2 = M.isSubmapOfBy (<=) (toMap b1) (toMap b2)

{-@ assume bagSize :: b:Bag k -> {i:Nat | i == bagSize b} @-}
bagSize :: Bag k -> Int
Expand Down

0 comments on commit 519cb5a

Please sign in to comment.