Zulip Chat Archive

Stream: new members

Topic: Angle brackets


view this post on Zulip Robert Spencer (Feb 01 2019 at 16:20):

Are (| ... |) and ⟨ ... ⟩ meant to be treated identically by lean?

view this post on Zulip Robert Spencer (Feb 01 2019 at 16:27):

In particular, I have a case where or.inr ⟨a, b⟩ works as expected, but or.inr (|a, b|) does not (it does though if I write or.inr ( (|a, b|) ).

view this post on Zulip Simon Hudon (Feb 01 2019 at 16:31):

That is curious. @Sebastian Ullrich, is this normal?

view this post on Zulip Sebastian Ullrich (Feb 01 2019 at 16:39):

It looks like (| is missing the precedence from

view this post on Zulip Sebastian Ullrich (Feb 01 2019 at 16:39):

i.e. it's a bug

view this post on Zulip Simon Hudon (Feb 01 2019 at 16:44):

Is it worth fixing?

view this post on Zulip Robert Spencer (Feb 01 2019 at 16:56):

Well, I'll file an issue, and then people can decide.

view this post on Zulip Mario Carneiro (Feb 01 2019 at 20:11):

issues at lean repo are dead on arrival for the most part. Everything I have seen suggests that lean ascii support is half-hearted at best and has several issues, and seems like one of those things that is more likely to be dropped than fixed in lean 4

view this post on Zulip Mario Carneiro (Feb 01 2019 at 20:12):

I recommend getting used to the angle brackets

view this post on Zulip Patrick Massot (Feb 01 2019 at 20:18):

This (| ... |) is a nightmare for mathematicians who want to use | for absolute values. I really really hope Lean 4 drops it

view this post on Zulip Robert Spencer (Feb 04 2019 at 07:01):

Hmmkay. That's a little disappointing personally as I am loathe to install an IDE just for unicode support.

view this post on Zulip Mario Carneiro (Feb 04 2019 at 07:18):

I mean, if you can find another means to input the unicode, by all means go ahead, but it's certainly easiest to use an editor that supports unicode

view this post on Zulip Mario Carneiro (Feb 04 2019 at 07:19):

You don't really need an IDE - I hesitate to call the existing editors IDEs since they are mostly just error reporting and unicode input

view this post on Zulip Mario Carneiro (Feb 04 2019 at 07:20):

but presumably you use some text editor to write your files, and you can probably set it up to input the lean unicode characters

view this post on Zulip Robert Spencer (Feb 04 2019 at 07:48):

This is true. I should just not be lazy and write some vimscript to translate \forall etc into unicode.

view this post on Zulip Robert Spencer (Feb 04 2019 at 07:50):

Although if it is the opinion of the maintainers that ASCII should not be preferred, it might be worth mentioning this in the tutorial document, and possibly throwing warnings that ASCII is deprecated (a bit more extreme)

view this post on Zulip Patrick Massot (Feb 04 2019 at 07:54):

You don't need any fancy vimscript, imap is all you need

view this post on Zulip Kevin Buzzard (Feb 04 2019 at 10:33):

Saved by a fellow vimmer :-) There are all sorts of people around here :-)


Last updated: May 14 2021 at 07:19 UTC