mathlib4 feat: `rename

trafficstars

Jul 21 '22 01:07 arthurpaulino

Also, I don't understand that lint error from the CI tests

Jul 21 '22 10:07 arthurpaulino

What's the reasoning behind changing the tactic from rename_var to rename_bvar?

Jul 24 '22 02:07 dwrensha

rename_var is not explicit enough and when looking at its name alone I was mistaken about its behavior. The fact is that this tactic only renames bound variables.

Jul 24 '22 12:07 arthurpaulino

I have a fix for this, but I don't have the necessary rights to push to this branch yet. @digama0 could I get these?

Jul 26 '22 14:07 JLimperg

I replaced your API for modifyLocalContext etc. with an API that is arguably more in line with the core APIs, though whether that makes it better is another question. Feel free to revert if you don't like it.

Jul 26 '22 15:07 JLimperg

@JLimperg

I replaced your API for modifyLocalContext etc. with an API that is arguably more in line with the core APIs, though whether that makes it better is another question. Feel free to revert if you don't like it.

I think there are benefits from having a function that already lives in MetaM to give more power to the user, no?

Jul 26 '22 15:07 arthurpaulino

Yes. The advantage of my API is that it works for any MonadMCtx and does not need to create additional metavariables. But there's certainly a tradeoff here. If you put my API in MetaM, you could get around the restriction that modifyMCtx only accepts a pure function; that might give you the best of both worlds.

Jul 26 '22 16:07 JLimperg

There are merge conflicts now.

bors d+