Stream: general

Topic: calc lhs/rhs

Johan Commelin (Nov 20 2018 at 14:42):

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 (Nov 20 2018 at 14:44):

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

Johan Commelin (Nov 20 2018 at 14:48):

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

Johan Commelin (Nov 20 2018 at 14:55):

Meeh, it's not really working...

MWE?

Johan Commelin (Nov 20 2018 at 15:01):

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 (Nov 20 2018 at 15:03):

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

Last updated: May 10 2021 at 19:16 UTC