Lars Hupel

It depends on how you construct such a set. One possibility to make it stack-safe would be to use a function `A => cats.Eval[Boolean]` instead of `A => Boolean`.

Strangely enough the Isabelle solver thinks `a` and `b` are terminating. Leon claims that `b(0)` doesn't terminate but Isabelle evaluates that to `false`. (I'm guessing because `i == 1` evaluates...

It turns out my assessment was wrong. Here's what Isabelle sees: ```isabelle fun a :: "int ⇒ int" and b :: "int ⇒ bool" where "a i = i -...

In essence, the question is: How do you deal with pre- and postconditions introducing complications in the call graph?

By the way, the Isabelle backend is supposed to _always_ give sound results even without `--termination` switched on. So there is definitely an issue here somewhere.

For the record, Isabelle complains about the datatype: ``` [Internal] Prover error in operation datatypes: ERROR Cannot define empty datatype "Core'2" ``` Unfortunately this check requires actually running Isabelle. There...

I would strongly recommend against going 3-only just yet. Cross-building for mouse shouldn't be a problem, no?

(The suggestion to use `withDottyCompat` in #149 is not at all a silver bullet)

The problem with a two-branch strategy is that it becomes impossible to ensure that both Scala 2 and Scala 3 builds are on par with features. Essentially, you are forcing...

Downstream consumers, no matter whether they're libraries or applications, will 100% be affected by your proposal. Essentially, even if there is source compatibility (which you cannot enforce if you have...