Yongshun Shreck Ye

I got this again about 1 or 2 months ago, too. And reinstalling everything doesn't seem to fix the problem.

See the code: ```agda open import Data.Nat ≤-trans : ∀ {m n p : ℕ} → m ≤ n → n ≤ p → m ≤ p ≤-trans m≤n n≤p...

I tried some more code and it seems it's more than that: case split also doesn't work with variable names with 3 or more characters. See the code: ```agda open...

> Hi @ShreckYe, > The problem may come with quoted benchmark function names with spaces. > Could you please check if that is the case for you? Thanks. I checked...

```kotlin fun CoroutineScope.coroutineToFuture( context: CoroutineContext = EmptyCoroutineContext, start: CoroutineStart = CoroutineStart.DEFAULT, block: suspend CoroutineScope.() -> T ): Future { val promise = Promise.promise() launch(context, start) { try { promise.complete(block()) }...

@bergmanngabor Thanks for your advice. I am not an expert in coroutine details either so it would be good that an actual expert weighed in here. As for the second...

OK, I will try to adapt them.

@vietj Hi Julien. It's done. Please review.

> There's some pretty neat additions proposed here that should help reduce boilerplate in most kotlin projects +1 Thank you.

I don't fully understand why the CI tests failed. Is it because that the "kotlin" source set in "vertx-lang-kotlin" is overriden by generated code?