Zulip Chat Archive

Stream: general

Topic: installing 3.4


Aron (May 27 2022 at 21:45):

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 (May 27 2022 at 21:46):

Lean 3.4? We're on 3.42 already

Aron (May 27 2022 at 21:47):

Ruben Van de Velde said:

Lean 3.4? We're on 3.42 already

Yes, 3.42.

Violeta Hernández (May 27 2022 at 21:47):

3.43 actually

Aron (May 27 2022 at 21:48):

Whichever one they stopped on.

Ruben Van de Velde (May 27 2022 at 21:48):

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

Henrik Böving (May 27 2022 at 21:48):

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 (May 27 2022 at 21:49):

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

Violeta Hernández (May 27 2022 at 21:49):

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

Violeta Hernández (May 27 2022 at 21:49):

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

Aron (May 27 2022 at 22:06):

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 (May 27 2022 at 22:10):

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 (May 27 2022 at 22:11):

Is it possible to do so without requiring BEq?

Henrik Böving (May 27 2022 at 22:18):

Sure the definition is straightforward:

def exunique (p : α  Prop) :=  (x : α), (p x   y, p y  x = y)

Arthur Paulino (May 27 2022 at 22:20):

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

Aron (May 28 2022 at 02:01):

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 (May 28 2022 at 03:27):

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

Eric Wieser (May 29 2022 at 20:39):

You need a lambda expression to bind l


Last updated: Dec 20 2023 at 11:08 UTC