Topic: calc lhs/rhs
Johan Commelin (Nov 20 2018 at 14:42):
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... But I'll try.
Johan Commelin (Nov 20 2018 at 14:55):
Meeh, it's not really working...
Bryan Gin-ge Chen (Nov 20 2018 at 14:58):
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):
pp.all is trimming my output. It is too long :rolling_on_the_floor_laughing:
Last updated: May 10 2021 at 19:16 UTC