search

leanprover / theorem_proving_in_lean

Theorem proving in Lean
Apache License 2.0
47 stars 46 forks source link

fix(dependent_type_theory.rst): typo #104

Closed agraboso closed 3 years ago

agraboso commented 4 years ago

In Σ x : α, β x, the type of (sigma.mk a b).2 is β (sigma.fst (sigma.mk a b)) and not β (sigma.snd (sigma.mk a b)).