Data.Bitvec.Basic !4#2179

Stream: mathlib4

[Shreyas Srinivas]

Thread for discussions about this PR

[Eric Wieser]

Note that this file was modified a month ago in #18131 in a way that depends on changes in port-status#data/fin/basic which haven't yet been forward-ported

[Eric Wieser]

I opened the forward-port PR a few hours ago at !4#2178.

[Eric Wieser]

port-status#data/bitvec/basic will shortly (~30 minutes) tell you the other problem: that the imports were recently changed in mathlib3, and you used mathport output from before that change propagated.

[Shreyas Srinivas]

uh oh

[Shreyas Srinivas]

What's the standard fix?

[Shreyas Srinivas]

The PR can't proceed without the ac_mono tactic in any case.

[Eric Wieser]

I would say the fix is wait for !4#2178, and wait for mathlib3port to rerun (which it does twice a day IIRC)