Probabilistic choice: Difference between revisions

Content added Content deleted

Inline

@@ Line 695: / Line 695: @@
                                           makeIntervalTree(assocs.run(midpoint)))
     } else {
-        def <nowiki>[[value, _]] := assocs</nowiki>
+        def [[value, _]] := assocs
         return leaf(value)
     }