Tesla Zhang‮

Fixed!

The plan is: + For data ctors, the order is random, but has to be linearizable. + For class fields, the order is as written. + Records are going to...

Is this done

/cc @wsx-ucb

Fixed!

I am now trying to implement this. Writing down some notes: + How to use classes: https://arxiv.org/pdf/2202.01629.pdf + Lean4: https://leanprover.github.io/lean4/doc/typeclass.html + https://arxiv.org/abs/2001.04301 + Jesper's idea on Agda instances: https://github.com/agda/agda/issues/6378 +...

After that we'll start playing with Sets: https://github.com/JetBrains/arend-lib/blob/master/src/Set.ard

Plan: + [x] Implement the non-core features of classes, like serialization, parsing, etc. (should be the first huge PR) + [ ] Deal with typing (mainly substitution) of field projections...

> What is the plan on this? It's probably abandoned. We will need to switch to using a proper JIT compiler and use the current core language directly for closures.

https://github.com/owo-lang/narc-rs/blob/master/src/syntax/surf/grammar.pest