Andreas Abel

(@phikal: Somehow your comment of 24 May was duplicated in the last comment.)

Btw, I played around with a leftist heap implementation in Agda and ended up with this: https://gist.github.com/andreasabel/352fee52a39c0bebbd5059bff86d9b6e This is 170 loc including comments, imports, and some auxiliary functions about adding...

Why doesn't this run through CI?

Yeah, Travis is dead, but there is a GHA CI now: https://github.com/UnkindPartition/tasty/blob/16289a77495eb8279c5e544886ef52503becd148/.github/workflows/ci.yaml Maybe it is misconfigured, it says `on: [push]` where I usually see `on: [push, pull_request]` or some refinement...

@adamgundry : I updated the CI triggers. Can you please rebase this onto `master` and force-push, to see if CI runs now?

Can't you use a `newtype` with a suitable `Eq` instance? (Ignoring that epsilon-distance isn't actually transitive, so it is not an equivalence relation.) ```haskell newtype Precision5 = Precision5 Double instance...

Yeah, maybe defining your own `assert...` functions/operators on top of `assertFailure` might be the way to go. Unless there is a clear consensus what the most common operators would be...

Dunno, but maybe ignoring unrecognized options with a warning rather than failing hard would be a more flexible and forward-compatible approach in a test suite runner like `tasty`?

Please rebase onto `master` and force-push to try and start CI.

I don't feel like I can make a judgement on whether this feature should be included. But I observe that no tests are included in this PR; and I think...