add complete queue property checks

[johnynek]

trying to exercise property checks by adding more checks for Queue. Definitely it can be tricky to implement functions in Bosatsu due to the totality requirements. For instance, implementing Rand::one_of was a bit tricky. You have to find the right recursion strategy. I was trying to make sampling O(log N), so I needed to make a tree. To do that, I used BinNat to be able to recur on half the size of the items, rather than the naive approach.

I also found a nice trick.

Define:

external def todo(ignore: x) -> forall a. a

then we can consume args and magically produce things by doing todo((foo, bar)) and run type-check. Then it fails at runtime since we don't actually implement todo. We could use this strategy except possibly make that function only exist in predef when running type-check (which doesn't output anything).

[codecov-commenter]

Codecov Report

All modified and coverable lines are covered by tests :white_check_mark:

Project coverage is 91.48%. Comparing base (04a0e87) to head (0cb4658). Report is 10 commits behind head on main.

:exclamation: Your organization needs to install the Codecov GitHub app to enable full functionality.

Additional details and impacted files

```diff @@ Coverage Diff @@ ## main #1171 +/- ## ========================================== + Coverage 91.32% 91.48% +0.16% ========================================== Files 96 96 Lines 11846 12010 +164 Branches 2675 2778 +103 ========================================== + Hits 10818 10987 +169 + Misses 1028 1023 -5 ```

:umbrella: View full report in Codecov by Sentry.
:loudspeaker: Have feedback on the report? Share it here.