Zulip Chat Archive

Stream: PR reviews

Topic: lean#227 pretty-print using dot notation


view this post on Zulip Gabriel Ebner (May 11 2020 at 14:20):

There was a thread in the newbies stream about eq.rhs, and how the .rhs is not pretty-printed in the tactic state (I'm not sure if I understood the comment correctly). This got me thinking, should we enable pp.generalized_field_notation by default? (It is not complete, and there are very likely cases where it doesn't round-trip.)

view this post on Zulip Reid Barton (May 11 2020 at 14:22):

Oh I didn't even notice this difference.

view this post on Zulip Johan Commelin (May 11 2020 at 14:24):

@Gabriel Ebner My comment was about something different:
I would like

h : x + y = z

and then

let L := h.lhs

should give

h : x + y = z
L := x + y -- and not h.lhs

view this post on Zulip Reid Barton (May 11 2020 at 14:24):

My point in that context was that you still see this term eq.rhs in some form, not the actual RHS of the equation (which you would see instead, if you had written it manually)

view this post on Zulip Johan Commelin (May 11 2020 at 14:24):

But that is orthogonal.

view this post on Zulip Patrick Massot (May 11 2020 at 14:24):

Yet another option I wasn't aware of...

view this post on Zulip Johan Commelin (May 11 2020 at 14:25):

Maybe we should add a reducibility setting transparent

view this post on Zulip Johan Commelin (May 11 2020 at 14:25):

@[transparent] def eq.lhs := ...

view this post on Zulip Gabriel Ebner (May 11 2020 at 14:25):

@Johan Commelin I get it now. Unfortunately I don't see a way to get this without adding a (local) notation.

view this post on Zulip Reid Barton (May 11 2020 at 14:25):

How do you do it with notation? I didn't see a way

view this post on Zulip Reid Barton (May 11 2020 at 14:25):

Another possibility is a pp flag to unfold reducible things

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

Or at least unfold transparent things

view this post on Zulip Gabriel Ebner (May 11 2020 at 14:26):

@Reid Barton You declare a notation that expands to a tactic, you can pass expressions to the tactic via the expected type.

view this post on Zulip Reid Barton (May 11 2020 at 14:26):

Johan Commelin said:

Maybe we should add a reducibility setting transparent

I feel like this would end up touching virtually everything for not that much benefit, though I could be wrong

view this post on Zulip Gabriel Ebner (May 11 2020 at 14:27):

I'm completely against making the pretty-printer unfold definitions. This is just going to cause lots and lots of confusion. There is a reason we don't beta-reduce during pretty-printing. However, having the elaborator unfold transparent definitions would be ok with me.

view this post on Zulip Reid Barton (May 11 2020 at 14:28):

pp.beta is one of my favorite options though...


Last updated: May 07 2021 at 19:12 UTC