Yongshun Ye

Autocompletion doesn't work with names containing operators, and case split doesn't work with names with one special character mixed with more characters or names with 3 or more characters

4

Agda supports special characters including Unicode characters in names except for reserved ones, and sometimes it's a convention to write names with such characters. Currently autocompletion and case split don't...

Should the Y combinator be pointed out in Untyped?

3

Should it be pointed out that the defined fixpoint in Untyped is well-known as the Y combinator, discovered by Haskell Curry? I learned about this the first time as the...

Currently, in Adequacy, there are `𝕍-sub`s and `𝔼-sub`s in the text and `sub-𝕍`s and `sub-𝔼`s in the code, which are inconsistent.

Can't build when used with Kotlin experimental features

3

The library I am benchmarking uses Kotlin's `ExperimentalUnsignedTypes`. I have already added ```kotlin @OptIn(ExperimentalUnsignedTypes::class) ``` to the benchmark class and ```kotlin tasks.withType().configureEach { kotlinOptions.freeCompilerArgs += "-Xopt-in=kotlin.RequiresOptIn" } ``` to `build.gradle.kts`...

Add some possibly useful code ported from https://github.com/huanshankeji/kotlin-common/tree/main/vertx

11

Motivation: Hi, Vert.x Maintainers. We have been developing our projects in Kotlin with the Vert.x toolkit as the core of the backend. It's been quite smooth and this project provides...

Official Kotlin library with "kotlinx" prefix?

2

Is this an official Kotlin library supported by JetBrains? If not, I guess it is not appropriate to use the "kotlinx" prefix in the name. It causes ambiguity.

Can't case split an `HitInt` with some already existing cases

1

"HitInt.agda": ```agda {-# OPTIONS --cubical --safe #-} module HitInt where open import Cubical.Data.Nat open import Cubical.Core.Everything open import Cubical.Foundations.Prelude using (subst) data ℤ : Set where pos : (n :...

Support polymorphic subclass serializers with inferred type arguments by refactoring `Serializer`s to bind to `KType`s instead of / in addition to `KClass`s

7

**What is your use-case and why do you need this feature?** The Kotlin compiler can infer some type arguments of a subtype from those of the parent abstract/sealed types. Currently,...