src/rules/correctness/pick.bend fails

rule pick: a def calls itself in a branch of a Bool.pick. Bool.pick is a function, so both branches are evaluated whatever the condition. In both branches, two recursive calls a step is 2^n work where one was meant (a per-token scan that took 20 s this way took 20 ms as one pass): bind the call once above the pick (+more = go(rest)) and pick between x <> more and more. In one branch, the recursion runs even when the other branch was the answer: a search never stops early and walks the whole input (portal-bend's get, bendoom's sorted insert). Match on the Bool instead, in a helper that takes it as a parameter. A self-call is the def's name followed by (..): a parameter or a value named like the def is not one. A pick nested in a branch of one already reported is not reported again; one nested in its condition is. A law file, a proof file and a def that is a proof never run, so they are exempt: a def that returns a proof, or one written with no type at all (def f(x, y):), which fills the law named f.