molikto

Can anyone comment what's needed to get this merged?

@mortberg it seems to me extension type requires subtyping. ``` def test (A : type ) (x y : A) (q : path A x y) : 𝕀 → A...

I always experienced the same thing from Renderscript (not this project) and never really solved it. What I do usually is just blur a bigger bitmap, so the artifacts will...

After sometime trying out, I think the parser should directly support formating, not as a plugin. For example, I am migrating some old notes from Pandoc, and `**$\omega$-accumulation point**` is...

I've been using it personally and satisfied with it, but I am no longer activity developing it anymore: * It is not a good suit for a commercial product: it...

I've been looking into operational transformation recently. This seems to be a good model for collaborative editing. I implemented it for Node = {String, List [Node]}, but got distracted by...

@AndrasKovacs if you are interested. I just finished HOAS to JVM bytecode https://github.com/molikto/mlang/blob/master/src-main/src/main/scala/mlang/compiler/PlatformEvaluator.scala#L903 it doesn't "full reduce" though, as in cubicaltt there is some compliciations.

also may I ask what exactly is "glued evaluator", my understanding is when solving meta, whnf is needed, a glued evaluator will be able to trace back to a much...

I just tried it: https://github.com/molikto/mlang/blob/master/library/01_foundations/00_builtin.poor forcing 10M seems not terminating in reasonable time forcing1M: // by value (branch full-reduction): polymorphic version: 5s, non-polymorphic version uses 79ms // by need (branch...

also this is what I do for reify https://github.com/molikto/mlang/blob/master/src-main/src/main/scala/mlang/compiler/semantic/10_value.scala#L122 basically it tries to see if this value is a whnf computed from other term, and the other term is used...