Tesla Zhang‮

It's a shame that this PR is not receiving developers' input. We have a smol library that modifies the java bytecode's java major version so that badass jlink still thinks...

Ohh! That's great! I take it all back. Nice job!!

> Thanks for the PR, @xzel23! Release 2.26.0 is out. Starting with this version, the plugin requires Gradle 7.0 or newer. > > As you all noticed, I didn't have...

```diff diff --git a/base/src/main/java/org/aya/tyck/StmtTycker.java b/base/src/main/java/org/aya/tyck/StmtTycker.java index 3b004b045..abf4838f7 100644 --- a/base/src/main/java/org/aya/tyck/StmtTycker.java +++ b/base/src/main/java/org/aya/tyck/StmtTycker.java @@ -6,6 +6,7 @@ import kala.collection.immutable.ImmutableSeq; import kala.collection.mutable.MutableArrayList; import kala.control.Either; import kala.control.Option; +import kala.value.MutableValue; import org.aya.concrete.Expr; import org.aya.concrete.Pattern;...

Reopen!

> > We already have it: [SyntaxHighlight.java](https://github.com/aya-prover/aya-dev/blob/279ca6f63dd87da81f1873a9066f6f59bd3217f9/lsp/src/main/java/org/aya/lsp/actions/SyntaxHighlight.java). But it needs some generalization. > > `SyntaxHighlight` looks don't add any links. Seems that we need to combine `SyntaxHighlight` and some code...

It would be nice if we can reuse these code. At least, `SyntaxHighlight` should be reused.

I agree. By `CoreDistiller` I probably only mean the pp of those `DefVar`s, which are still present in concrete

Closing for now, because the rules are implemented. Coercions are yet to be done.

Do you still remember what is this?