Random Lean experiments
name = "leantest" version = "0.1.0" defaultTargets = ["leantest"] [[lean_lib]] name = "Leantest" [[lean_exe]] name = "leantest" root = "Main" [[require]] name = "mathlib" scope = "leanprover-community"