Mechanism for configuring the number of tests run when doing randomized search

[byorgey]

For example (this is using the yet-unmerged prop branch):

Disco> holds (exists a:N,b:N,c:N. (0 < a < b < c) and (a^2 + b^2 == c^2))
true
Disco> :test (exists a:N,b:N,c:N. (0 < a < b < c) and (a^2 + b^2 == c^2))
  - No example was found: ∃ a, b, c. 0 < a < b < c and a ^ 2 + b ^ 2 == c ^ 2
    Checked 100 possibilities.

It would be nice in this case to be able to crank up the number of tests (which is currently hardcoded to 100) enough to be able to find an example.

[byorgey]

Note that whatever mechanism we come up with, it should be usable with both the :test command and with !!! properties.

Maybe just a built-in primitive function testWith : N * Prop -> Prop? Hmm, no, that feels weird because the number of test cases is not an inherent semantic property of a proposition. It is runtime configuration.

What about this: we define syntax for a "configured test" to be something like {! <options> !} <Prop>, but where options part is optional. Then both :test and !!! will take a "configured test". So you could write something like e.g.

:test {! numTests = 1000 !} exists a:N, b:N, c:N. (0 < a < b < c) and (a^2 + b^2 == c^2)