Comments on the form:

• You should add a header, with the license details and so on, but also explaining what is in the file, with motivations, math explanations, and references to the literature.
• Add docstrings to most of the definitions
• You should use namespaces: put the first definitions in the filter namespace, and the instances maybe in filter.bigly_equal.

Otherwise, the maths look good (except that you are missing a field instance when your filter is a ultrafilter).

@abhimanyupallavisudhir I already made the fix and checked compilation on my machine. I am just waiting for the Travis check to finish, and then I'll merge.

@abhimanyupallavisudhir I already made the fix and checked compilation on my machine. I am just waiting for the Travis check to finish, and then I'll merge.

Isn't making f implicit a better fix?

@abhimanyupallavisudhir I didn't even see your change. I think we pushed them at the same time. Could you make the argument implicit again and adapt @jcommelin's suggestions as you see fit? Then I'll merge right away.

Ok, all done.