calc lhs/rhs

Stream: general

[Johan Commelin]

When writing calc blocks, it would be very convenient if we could have some special symbol that refers to the lhs/rhs of the original goal. Because currently I try to copy paste stuff from the goal, and then Lean starts moaning that it can't figure out the type etc...
I guess it might be tricky to use literal lhs, because people might want to use that as variable name. But maybe something can be done?

[Bryan Gin-ge Chen]

I've been using _ to start / end calc blocks with the lhs / rhs.

[Johan Commelin]

Hmm, I fear that it will then start moaning about X in _ = X... But I'll try.

[Johan Commelin]

Meeh, it's not really working...

[Bryan Gin-ge Chen]

MWE?

[Johan Commelin]

Well... I don't really know how to produce a MWE. I'm not going to trim down my sheaf branch... I guess I could just enable pp.all and copy-paste the lhs into the calc-block. It's just more convenient if there would be a shorthand for it.

[Johan Commelin]

Fail... pp.all is trimming my output. It is too long :rolling_on_the_floor_laughing: