installing 3.4

Stream: general

[Aron]

elan doesn't seem to have any documentation for installing 3.4, and there's no example sheets for lean4 so I don't feel like using it...
any tips?

[Ruben Van de Velde]

Lean 3.4? We're on 3.42 already

[Aron]

Ruben Van de Velde said:

Lean 3.4? We're on 3.42 already

Yes, 3.42.

[Violeta Hernández]

3.43 actually

[Aron]

Whichever one they stopped on.

[Ruben Van de Velde]

Either I'm living in the past, or Violeta is living in the future :)

[Henrik Böving]

That and If you're just not interested in Lean 4 because there are no examples, we have quite a nice ressource available here already: https://leanprover.github.io/theorem_proving_in_lean4/ the reason people pick Lean 3 over 4 at the moment is mostly that the former has mathlib while the latter doesnt have mathlib but all the sparkly new features.

[Violeta Hernández]

Lean 3.4 is the last "official" version, but the community has been maintaining the core library in the meanwhile

[Violeta Hernández]

And those "non-official" versions are the ones used by mathlib

[Violeta Hernández]

So they're basically official as far as I care :P

[Aron]

On an unrelated note, how would I use the usual toolchain to write "exists unique" in lean4? \ex ! doesn't seem to work. Is exunique not implemented in lean4?

[Henrik Böving]

Its at least no implemented in the core library, I dont know if its in the mathlib4 stub from the top of my head (though it would of course be easy to define yourself)

[Arthur Paulino]

Is it possible to do so without requiring BEq?

[Henrik Böving]

Sure the definition is straightforward:

def exunique (p : α → Prop) := ∃ (x : α), (p x ∧ ∀ y, p y → x = y)

[Arthur Paulino]

Oh, right, I confused some concepts! Thanks :D

[Aron]

Henrik Böving said:

Sure the definition is straightforward:

def exunique (p : α → Prop) := ∃ (x : α), (p x ∧ ∀ y, p y → x = y)

Trying to apply it is causing problems.

def exunique (p : α → Prop) := ∃ (x : α), (p x ∧ ∀ y, p y → x = y)


class incidence (point line: Type) (inc:point → line → Prop) :=
(one:∀ P Q, P ≠ Q → exunique (l:line) (inc P l ∧ inc Q l))

application type mismatch
  exunique l
argument
  l
has type
  line : Type
but is expected to have type
  ?m.93 → Prop : Sort (max 1 ?u.92)

[Kevin Buzzard]

Is this Lean 4? You might have more luck on the #lean4 stream

[Eric Wieser]

You need a lambda expression to bind l