congrm

Stream: PR reviews

[Patrick Massot]

Is there anything blocking #2544?

[Scott Morrison]

Lack of attention so far, unfortunately. :-(

[Moritz Doll]

there is a bit of the question where to move some of the functions that are not specific to congrm to and also whether their design is good. I made PRs for that in std4, but they not moved either (std4#146). If it is decided that this should be going into mathlib first and not into std4, then I can happily merge the changes into the congrm PR. I just need to know which is the correct folder for the functions.