Recent Commits to lean4:master

Stream: general

[Patrick Massot]

rss-bot said:

doc: add lean3changes.md
doc: add lean3changes.md
https://github.com/leanprover/lean4/commit/cf7779936419085093ab0ea20f4738dd08030f90

For people not following the rss stream: this is nice to read (follow the link to this file).

[Yury G. Kudryashov]

I see that Lean 4 uses · for lambdas, so we'll have to find another symbol for smul.

[Reid Barton]

At one point I suggested stealing the symbol used by the "stupid triangle", and using its mirror image for right actions.

[Johan Commelin]

https://en.wikipedia.org/wiki/Interpunct#Similar_symbols

[Eric Wieser]

· (lean4) is not the same as •(smul) though? Do you mean matrix multiplication needs a new symbol?

[Yury G. Kudryashov]

Eric Wieser said:

· (lean4) is not the same as •(smul) though? Do you mean matrix multiplication needs a new symbol?

I mean that I should read more carefully.

[Floris van Doorn]

More got added to the file today (About dependent functions and meta).

[Floris van Doorn]

I'm happy to see the notation(x : α) → β x for the dependent function type.

[Mario Carneiro]

We can still write forall (x : α), β x and ∀ (x : α), β x, but the parentheses are not optional when the type is provided explicitly.

@Sebastian Ullrich Why is this?

[Kevin Lacker]

the keyword meta is removed from lean 4 eh. so how should a meta function get migrated from lean 3 to lean 4, do you just directly replace it with unsafe ?

[Kevin Lacker]

i am also curious if anyone working on lean 4 has done profiling to estimate the speed differences between 3 -> 4

[Mario Carneiro]

Speed of what? We would like to benchmark a large library because that's what we want, but there is a whole lot of infrastructure missing before we can even mock something up that is reasonably close to mathlib

[Mario Carneiro]

Obviously tactics are going to be orders of magnitude faster, as they are compiled now, but the way that they interact with the elaborator and such in proofs is as yet untested because there aren't any nontrivial proofs in lean 4

[Chris B]

Kevin Lacker said:

i am also curious if anyone working on lean 4 has done profiling to estimate the speed differences between 3 -> 4

There are some benchmarks comparing Lean 4 to other programming languages (but not Lean 3) in this paper: https://arxiv.org/abs/1908.05647

[Eric Wieser]

I'm happy to see the notation(x : α) → β x for the dependent function type.

I can see two annoying ways this will impact mathlib now:

• pi as a file name will be much less obvious, since the pi symbol is no longer used
• There won't be a symbol available for dfinsupp to distinguish it from finsupp while still looking like a regular function

[Anne Baanen]

"Easy" fixes: rename pi to function and use dfinsupp instead of finsupp everywhere. :stuck_out_tongue_wink:

[Patrick Massot]

The second half is unfortunately likely to cause elaboration issues

[Mario Carneiro]

I think they are called pi types in agda too despite the arrow notation

[Mario Carneiro]

Does this mean that sigma types are (x : α) × β x now?

[Sebastian Ullrich]

Mario Carneiro said:

We can still write forall (x : α), β x and ∀ (x : α), β x, but the parentheses are not optional when the type is provided explicitly.

Sebastian Ullrich Why is this?

I don't know what you're talking about :grinning_face_with_smiling_eyes: https://github.com/leanprover/lean4/commit/7e8a7e6660292cb9d93e79df64cabecb4e14aa27