How can I learn types?

Stream: new members

[İmran Tanrikolu]

How can I learn and master dependent type theory and the propositions-as-types concept? Where can I find theories proven on Lean, from easy to advanced, to study? Which types do I need to learn and master for Lean?

[Kenny Lau]

these are rather broad questions, and this is just my advice, maybe I would start from (intuitionistic?) propositional logic (i.e. zeroth order), for example (i just made this up), try proving the following (i'll give you all the tools):

variable (P Q R : Prop)

#check And.intro
#check And.left
#check And.right

example (h₁ : P → Q) (h₂ : P) : Q :=
  h₁ h₂

theorem And.symm' (h : P ∧ Q) : Q ∧ P :=
  _

[Kenny Lau]

try to replace _ there with a correct term using the tools given

[Kenny Lau]

(it's also useful to look at the "expected type" window, which is by default collapsed on the website)

[İmran Tanrikolu]

Kenny Lau dedi:

(it's also useful to look at the "expected type" window, which is by default collapsed on the website)

Actually, what I mean is: where can I study type theory? It can be a book or another resource. Also, where can I find Lean proofs that I can study from simple to advanced?
I am currently learning and cannot fully write code myself yet. I am about to finish the Lean Number Game and looking for new resources.

[Kenny Lau]

https://leanprover.github.io/theorem_proving_in_lean4/#

[Kenny Lau]

people recommend this

[İmran Tanrikolu]

Kenny Lau dedi:

people recommend this

Thanks! By the way, do you have any recommendations on where I can find exercises and example problems? Any advice?

[Kenny Lau]

hmm, that's a good idea, we should have some exercises, i don't know if they exist

[Kenny Lau]

for now... i guess try to reproduce the book lol