type system

Stream: general

[Enrico Borba]

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.

[Johan Commelin]

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

[Johan Commelin]

That's the default reference, I think

[Enrico Borba]

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