refactor: further simplification

src/lake/Lake/CLI/Init.lean

@@ -93,17 +93,17 @@ def mathConfigFileContents (pkgName libRoot : String) :=
 s!"import Lake
 open Lake DSL
 
-def moreServerArgs := #[
+-- Settings applied to both builds and interactive editing
+def basicLeanArgs := #[
   \"-Dpp.unicode.fun=true\", -- pretty-prints `fun a ↦ b`
   \"-Dpp.proofs.withType=false\"
 ]
 
--- These settings only apply during `lake build`, but not in VSCode editor.
-def moreLeanArgs := moreServerArgs
-
 package {pkgName} where
-  moreServerArgs := moreServerArgs
-  moreLeanArgs := moreLeanArgs
+  -- Settings applied only to interactive contexts (e.g., the VSCode editor)
+  moreServerArgs := basicLeanArgs
+  -- Settings applied only to a build (e.g., via `lake build`)
+  moreLeanArgs := basicLeanArgs
   -- add additional package configuration options here
 
 require mathlib from git