Tesla Zhang‮

> I'd say adding them as explicit parameters to constructors and projectors will be the best choice ( But that's gonna lead to inconsistency between constructors and patterns. I'd like...

@AD1024 @zyh3838438zyh :wink:

> Typecheck ok gives 🐮🍺, and qutting REPL gives 🍵. I'm not doing this right now -- 🍵 is the output for scope-check failure. I tried 🌶🐔, but both Windows...

> I see, I thought `narc-rs` would be superseding the `voile-rs` so I am expecting the row polymorphism feature. Got it! I did some minor research in the first year...

But this language is not intended to be debugged a lot anyway

Checkout the commit log, you'll see she deletes some binary file, that's it

The current implementation of universe level does not satisfy: > Luo also adds a rule for function types which is covariant in the codomain but demands equality in the domain....

Neither minitt-rs nor voile-rs has termination check. If you wanna have a try, I'll recommend working on Voile because of the term structure. In Voile, the `Neutral::App` AST element is...

Yes, sized vector is a well-known instance of GADT. This will be implemented in Narc along with dependent pattern matching.

Do you have overlapping pattern (and confluence check) support? I am quite interested.