!4#4872 Data.Real.Pi.Bounds

Stream: PR reviews

[Ruben Van de Velde]

This needs some small tactic work. Maybe the kind @Damiano Testa enjoys? :)

[Damiano Testa]

Ruben, you are right, this does sound fun! I'll try to take a look, but I do not have much time, so it may take a while...

[Damiano Testa]

I made a very crude port of the tactic part of the file: locally it seems to build and I pushed it through EDIT[it passes] CI.

[Damiano Testa]

I labelled it as awaiting-review. I also added the meta label, although I am not sure if this is appropriate.

[Damiano Testa]

I'm sorry, but I've broken the merge of the PR by pushing a golfing change, while it was being merged.

Can someone put it back on the queue, please?