Zulip Chat Archive

Stream: general

Topic: type system


view this post on Zulip Enrico Borba (Jan 14 2020 at 08:56):

Is there a good paper or resource on Lean’s type system? It kind of blows my mind how much can be inferred / elaborated. When I was researching type systems, inference becomes undecidable quickly if you allow for “too much” polymorphism. So I’m interested in learning more about what type systems Lean’s is based off of.

view this post on Zulip Johan Commelin (Jan 14 2020 at 08:57):

https://github.com/digama0/lean-type-theory/releases

view this post on Zulip Johan Commelin (Jan 14 2020 at 08:57):

That's the default reference, I think

view this post on Zulip Enrico Borba (Jan 14 2020 at 08:59):

Fantastic, I don’t know why I had a hard time googling this. Thank you!


Last updated: May 17 2021 at 23:14 UTC