kevinzz

4 ms·

1. 1.▲
   by kevinzz 7y ago

   Lean 4 is no longer being developed in private; this was true a year ago but is no longer true. What is true is that Lean 4 is still not ready for the port of the maths library to begin, and we do not know when it will be. Furthermore, one
2. 2.▲
   by kevinzz 7y ago

   There is every way of knowing how much will be obsolete in Lean 4, as long as you're following the discussions at https://leanprover.zulipchat.com . The type theory of Lean 4 will be the same as Lean 3, there are some minor
3. 3.▲
   by kevinzz 7y ago

   The headline is clickbait. A more measured debate about the issues is here https://xenaproject.wordpress.com/2019/09/27/does-anyone-kno...
4. 4.▲
   by kevinzz 7y ago

   https://xenaproject.wordpress.com/2019/09/27/does-anyone-kno...
5. 5.▲
   by kevinzz 8y ago

   In Lean you could do theorem and_commutative (p q : Prop) : p ∧ q → q ∧ p := by cc for a tactic proof and theorem and_commutative (p q : Prop) : p ∧ q → q ∧ p := λ ⟨h,j⟩,⟨j,h⟩ for a term proof (just write down the function).