Tesla Zhang‮

I highly recommend a modern identity type (beyond jmeq or mltt id). Quotients and funExt are essential.

I suggest observational equality by McBride or cubical extension type (either cartesian or de morgan)

> **Solution 2:** > > We might implement constraints-based unification. I have a feeling that this is just pattern unification. Can you tell me what makes it different?

But it looks like the most general solution isn't it?

@xieyuheng So, in case of multiple solutions, it is sound to always pick the most general one (if exists), no?

Cool!!

Cool!!

Thanks!

@CodeDead no, gradle can run on jdk 17 and build a project using another jdk which is jdk 19. Gradle 7.6 will add support for running gradle on JDK 19,...

> @ice1000 & @xzel23 yes, but isn't this quite difficult to achieve with automated builds like GitHub Actions, Jenkins and the likes since you will need dual JDK's installed in...