Maximum number of WithTops

Stream: mathlib4

[Geoffrey Irving]

This is a very silly question, but I’m curious: what is the maximum number of stacked WithTops in Mathlib? E.g., ContDiffAt involves 2, as the order of differentiability WithTop (WithTop Nat)) for finite or smooth or analytic.

Not quite sure how to search for it since as in the ContDiffAt case it can be hidden: there it’s written as WithTop ℕ∞.

[Michael Rothgang]

It's a fun question, though. I'm not sure what the answer is, but am also curious.

[Michael Rothgang]

You could certainly write a metaprogramm that looks for all WithTop instances, and then recursively determines the maximum depth.

[Geoffrey Irving]

I guess the simplest way is walking through the cached o files? Or I guess just everything in scope after import Mathlib?

[Michael Rothgang]

import Mathlib should reach everything we care about, indeed.