infinite.nat.infinite

Stream: general

[Yaël Dillies]

Why is docs#infinite.nat.infinite having such a name? The instance is left unnamed in the code. I thought unnamed instances didn't pick up namespaces?

[Eric Wieser]

They pick up namespace but eliminate them if they're a duplicate

[Eric Wieser]

The naming heuristic expects that to be declared in the root or nat namespace.

[Eric Wieser]

Not the infinite namespace.