check out mlang

Stream: general

[Minghao Liu]

Hello. I am working on a new cubical type implementation, and wrote a note might be relevant to lean users. something I call elaboration calculus. it atempts to solve some problem mentioned in "A Review of the Lean Theorem Prover". If you are familar with dependent type implementations, and found it interesting, maybe we can discuess it!

[Jason Rute]

(Deleted)

[Mario Carneiro]

the link works for me, and your link is identical to the original?

[Jason Rute]

I think it is just the Zulip app on my iPhone. It inserts an extra 25 into the URL. Anyway, if I copy the link it is fine.