Skip to content

Commit

Permalink
Fixing linting issues.
Browse files Browse the repository at this point in the history
  • Loading branch information
Matthew-Mosior committed Sep 19, 2024
1 parent 5586d97 commit 953a4ce
Show file tree
Hide file tree
Showing 5 changed files with 8 additions and 8 deletions.
2 changes: 1 addition & 1 deletion profile/src/Main.idr
Original file line number Diff line number Diff line change
Expand Up @@ -323,7 +323,7 @@ bench = Group "containers"
[ Single "1" (basic createSortedSet 0)
, Single "100" (basic createSortedSet 99)
, Single "1000" (basic createSortedSet 999)
]
]
, Group "insertMap"
[ Single "10" (basic insertMap 0)
]
Expand Down
2 changes: 1 addition & 1 deletion src/Data/Map.idr
Original file line number Diff line number Diff line change
Expand Up @@ -1329,7 +1329,7 @@ fromList xs =
in case rest of
[] =>
assert_total $ idris_crash "Unexpected empty list"
(middle :: right) =>
(middle :: right) =>
(left, middle, right, len)
-- Build a balanced tree from a non-empty list
buildBalancedTree : List1 (k, v) -> Nat -> Map k v
Expand Down
2 changes: 1 addition & 1 deletion src/Data/Map/Internal.idr
Original file line number Diff line number Diff line change
Expand Up @@ -50,7 +50,7 @@ singleton k x = Bin 1 k x Tip Tip
export
size : Map k v -> Nat
size Tip = 0
size (Bin _ _ _ l r) = 1 + size l + size r
size (Bin _ _ _ l r) = 1 + size l + size r

--------------------------------------------------------------------------------
-- Map Internals
Expand Down
6 changes: 3 additions & 3 deletions src/Data/Set.idr
Original file line number Diff line number Diff line change
Expand Up @@ -603,7 +603,7 @@ partial
findMin : Set a -> a
findMin t =
case lookupMin t of
Just r => r
Just r => r
Nothing => assert_total $ idris_crash "Set.findMin: empty set has no minimal element"

||| The maximal element of the set. Calls idris_crash if the set is empty. O(log n)
Expand Down Expand Up @@ -724,7 +724,7 @@ intersection t1@(Bin _ x l1 r1) t2 =
let (l2,x',r2) = splitMember x t2
l1l2 = intersection l1 l2
r1r2 = intersection r1 r2
in case x' of
in case x' of
True =>
case l1l2 == l1 && r1r2 == r1 of
True =>
Expand Down Expand Up @@ -790,7 +790,7 @@ fromList xs =
in case rest of
[] =>
assert_total $ idris_crash "Unexpected empty list"
(middle :: right) =>
(middle :: right) =>
(left, middle, right, len)
-- Build a balanced tree from a non-empty list
buildBalancedTree : List1 a -> Nat -> Set a
Expand Down
4 changes: 2 additions & 2 deletions src/Data/Set/Internal.idr
Original file line number Diff line number Diff line change
Expand Up @@ -40,7 +40,7 @@ singleton x = Bin 1 x Tip Tip
export
size : Set a -> Nat
size Tip = 0
size (Bin _ _ l r) = 1 + size l + size r
size (Bin _ _ l r) = 1 + size l + size r

--------------------------------------------------------------------------------
-- Set Internals
Expand Down Expand Up @@ -197,7 +197,7 @@ minViewSure : a -> Set a -> Set a -> (a,Set a)
minViewSure x Tip r = (x,r)
minViewSure x (Bin _ xl ll lr) r =
case minViewSure xl ll lr of
(xm, l') =>
(xm, l') =>
(xm, balanceR x l' r)

export
Expand Down

0 comments on commit 953a4ce

Please sign in to comment.