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