name = "Example" version = "0.1.0" [leanOptions] autoImplicit = false [[require]] name = "mathlib" scope = "leanprover-community" rev = "v4.15.0"