Tesla Zhang‮

> It is still in progress. Thanks for the reply! Really appreciate this work!

Nice!

It would be interesting to see if virtual threads can bring any benefit to IntelliJ platform

Closed because the YouTrack ticket has been closed!

Match should probably be done after termination check IMO

https://github.com/JetBrains/Arend/blob/master/base/src/main/java/org/arend/typechecking/covariance/CovarianceChecker.java

> Smaller code: > > ``` > open data Unit | unit > open data Nat | O | S Nat > open data SomeDT Nat > | m =>...

> > because mathematicians may want to use them. > > Is there any example? I recall that's what happened to Lean 4, they switched their lambda syntax to `fun...

I think this is fixed already

Idea: + We'd rather not have any ways to specify tighter/looser in infixes, because the syntax is ugly. + Infix parameters always bind the tightest, loosest, or they have no...