Zulip Chat Archive

Stream: general

Topic: calc lhs/rhs


view this post on Zulip 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?

view this post on Zulip Bryan Gin-ge Chen (Nov 20 2018 at 14:44):

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

view this post on Zulip 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.

view this post on Zulip Johan Commelin (Nov 20 2018 at 14:55):

Meeh, it's not really working...

view this post on Zulip Bryan Gin-ge Chen (Nov 20 2018 at 14:58):

MWE?

view this post on Zulip 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.

view this post on Zulip 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