You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
dataHeap:Type->TypewhereEmpty:Ord elem=> Heap elem
Node:Ord elem=> Int -> elem -> Heap elem -> Heap elem -> Heap elem
merge: Heap elem -> Heap elem -> Heap elem
merge heap Empty= heap
merge Empty heap = heap
merge h1@(Node_ elem1 left1 right1) h2@(Node_ elem2 left2 right2) =if elem1 <= elem2
then makeT elem1 left1 (merge right1 h2)
else makeT elem2 left2 (merge h1 right2)
whererank: Heap elem -> Int
rank Empty=0
rank (Node r ___) = r
makeT: elem -> Heap elem -> Heap elem -> Heap elem
makeT x left right =if rank left >= rank right
thenNode (rank right +1) x left right
elseNode (rank left +1) x right left
$ idris2 --check Heap.idr
Expected Behavior
1/1: Building Heap (Heap.idr)
Observed Behavior
1/1: Building Heap (Heap.idr)
Heap.idr:19:34--20:29:While processing right hand side of Main.merge at Heap.idr:8:1--21:1:
While processing right hand side of 1148:makeT at Heap.idr:18:5--21:1:
Multiple solutions found in search. Possible correct results:
conArg
conArg
The text was updated successfully, but these errors were encountered:
The error message is bad, but there are definitely two possible results: one from the first Node, one from the second. There's no guarantee they'd be the same.
Steps to Reproduce
Heap.idr
:Expected Behavior
Observed Behavior
The text was updated successfully, but these errors were encountered: