Type theory types and lemmas in std/mathlib?

Stream: new members

[aron]

I'd like to experiment with type systems, trying to see if I can implement my own, exploring different types systems and so on.

Are there any types/constructs for this in the Stdlib or Mathlib? Where would be the best place for me to start looking?

[aron]

(btw I am not a mathematician so if in doubt pls err on the side of assuming I don't know something than vice versa :sweat_smile:)

[Luigi Massacci]

I would rather suggest ditching lean all together, and looking at things like Software Foundations (Volume 2 in particular) which is based on Coq.

[Luigi Massacci]

Another big classic is Programming in Martin-Lof Type Theory which has a bunch of examples in ML (this is a bit old though)

[Luigi Massacci]

Personally I really enjoyed Program == Proof by Samuel Mimram which has plenty of examples in Ocaml and Agda

[Luigi Massacci]

For experimenting with type theory, I'd say you are much better off with Coq and Agda, as those communities are heavily interested in that kind of stuff so there's a lot more material out there