lean#227 pretty-print using dot notation

Stream: PR reviews

[Gabriel Ebner]

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]

Oh I didn't even notice this difference.

[Johan Commelin]

@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]

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]

But that is orthogonal.

[Patrick Massot]

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

[Johan Commelin]

Maybe we should add a reducibility setting transparent

[Johan Commelin]

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

[Gabriel Ebner]

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

[Reid Barton]

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

[Reid Barton]

Another possibility is a pp flag to unfold reducible things

[Johan Commelin]

Or at least unfold transparent things

[Gabriel Ebner]

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

[Reid Barton]

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]

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]

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