Zulip Chat Archive

Stream: general

Topic: heresy

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.

Reid Barton (May 26 2020 at 13:24):

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

Johan Commelin (May 26 2020 at 13:32):

@Reid Barton Because it's less recognizable?

Johan Commelin (May 26 2020 at 13:33):

There's also ⦑dotted angle brackets⦒

Reid Barton (May 26 2020 at 13:33):

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

Johan Commelin (May 26 2020 at 13:33):

Why not? Muscle memory?

Johan Commelin (May 26 2020 at 13:34):

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

Reid Barton (May 26 2020 at 13:35):

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

Johan Commelin (May 26 2020 at 13:37):

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

Gabriel Ebner (May 26 2020 at 13:37):

Are ⟨ and ⟨ different?

Johan Commelin (May 26 2020 at 13:37):

@Gabriel Ebner How would I know? :rofl:

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.

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.