batteries icon indicating copy to clipboard operation
batteries copied to clipboard

Published 20 hours ago • verified publisher icon leanprover-community

chore: upstream spread syntax `__ :=`

Open kim-em opened this issue 2 years ago • 2 comments

kim-em avatar Sep 06 '23 23:09 kim-em

I don't really like this being an extension to all structure instances, it's a potential performance issue. Is there a reason this can't or shouldn't be upstreamed to core?

digama0 avatar Jan 05 '24 05:01 digama0

No, I think that would be reasonable. I'll mark this as help-wanted in the hope that someone is interested in taking this on!

kim-em avatar Jan 05 '24 05:01 kim-em