name = "brooks" defaultTargets = ["Brooks"] [[lean_lib]] name = "Brooks" [[require]] name = "mathlib" scope = "leanprover-community" rev = "v4.18.0"