Stream: PR reviews

Topic: lean#227 pretty-print using dot notation

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.)

Reid Barton (May 11 2020 at 14:22):

Oh I didn't even notice this difference.

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

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)

Johan Commelin (May 11 2020 at 14:24):

But that is orthogonal.

Patrick Massot (May 11 2020 at 14:24):

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

Johan Commelin (May 11 2020 at 14:25):

Maybe we should add a reducibility setting transparent

Johan Commelin (May 11 2020 at 14:25):

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

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.

Reid Barton (May 11 2020 at 14:25):

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

Reid Barton (May 11 2020 at 14:25):

Another possibility is a pp flag to unfold reducible things

Johan Commelin (May 11 2020 at 14:26):

Or at least unfold transparent things

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.

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

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.

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