Zulip Chat Archive

Stream: general

Topic: heresy


view this post on Zulip Johan Commelin (May 26 2020 at 13:23):

I propose a heresy: we map \( and \) to ⦇x,y,z⦈ and use this for anonymous constructors. This frees up \< and \> for inner products and such.

view this post on Zulip Reid Barton (May 26 2020 at 13:24):

how about just using ⦇x,y⦈ for the inner product

view this post on Zulip Johan Commelin (May 26 2020 at 13:32):

@Reid Barton Because it's less recognizable?

view this post on Zulip Johan Commelin (May 26 2020 at 13:33):

There's also ⦑dotted angle brackets⦒

view this post on Zulip Reid Barton (May 26 2020 at 13:33):

OK, but changing \< and \> can't be a serious suggestion I hope.

view this post on Zulip Johan Commelin (May 26 2020 at 13:33):

Why not? Muscle memory?

view this post on Zulip Johan Commelin (May 26 2020 at 13:34):

We could keep \< and \> for the anonymous constructor, and \langle and \rangle for inner product notation

view this post on Zulip Reid Barton (May 26 2020 at 13:35):

Also breaking basically every line of Lean source ever, as well as documentation, etc.

view this post on Zulip Johan Commelin (May 26 2020 at 13:37):

Maybe ❬medium angle bracket ornament❭ is good enough for inner products

view this post on Zulip Gabriel Ebner (May 26 2020 at 13:37):

Are and different?

view this post on Zulip Johan Commelin (May 26 2020 at 13:37):

@Gabriel Ebner How would I know? :rofl:

view this post on Zulip Reid Barton (May 26 2020 at 13:38):

If there is a difference, it didn't survive being copied and pasted into emacs in a tmux session.

view this post on Zulip Yury G. Kudryashov (May 26 2020 at 14:33):

/me would prefer if Lean used 〈 LEFT-POINTING ANGLE BRACKET not ⟨ MATHEMATICAL LEFT ANGLE BRACKET for anonymous constructors leaving "MATHEMATICAL" part of Unicode to mathlib but I I think that breaking compatibility here is a bad idea.

view this post on Zulip Johan Commelin (May 26 2020 at 14:36):

/me vehemently agrees with @Yury G. Kudryashov

view this post on Zulip Johan Commelin (May 26 2020 at 14:36):

@Sebastian Ullrich Is this heresy still fixable in :four_leaf_clover: ?

view this post on Zulip Sebastian Ullrich (May 26 2020 at 14:39):

They look exactly the same in my editor...

view this post on Zulip Andrew Ashworth (May 26 2020 at 14:47):

why not bra-ket notation?

view this post on Zulip Ryan Lahfa (May 26 2020 at 22:38):

Is a syntax like(x | y) possible?

view this post on Zulip Ryan Lahfa (May 26 2020 at 22:39):

(in France, this is somewhat a classical notation for inner products, non-hermitian ones at least.)

view this post on Zulip Ryan Lahfa (May 26 2020 at 22:40):

Ah, I guess it is not because of the status of | in Lean…

view this post on Zulip Johan Commelin (May 27 2020 at 05:10):

Well, there are other unicode versions of |

view this post on Zulip Ryan Lahfa (May 27 2020 at 06:22):

Johan Commelin said:

Well, there are other unicode versions of |

Let's not get into that :-D…


Last updated: May 08 2021 at 19:11 UTC