diff --git a/src/Lean/Parser/Command.lean b/src/Lean/Parser/Command.lean index 35af9ce35a..39bffdd827 100644 --- a/src/Lean/Parser/Command.lean +++ b/src/Lean/Parser/Command.lean @@ -90,7 +90,7 @@ def declValEqns := leading_parser def whereStructField := leading_parser Term.letDecl def whereStructInst := leading_parser - " where" >> sepByIndent (ppGroup whereStructField) "; " (allowTrailingSep := true) >> + ppIndent ppSpace >> "where" >> sepByIndent (ppGroup whereStructField) "; " (allowTrailingSep := true) >> optional Term.whereDecls /- Remark: we should not use `Term.whereDecls` at `declVal` diff --git a/src/Lean/Parser/Term.lean b/src/Lean/Parser/Term.lean index 5ec53c71a3..5da2743c25 100644 --- a/src/Lean/Parser/Term.lean +++ b/src/Lean/Parser/Term.lean @@ -495,7 +495,7 @@ def «letrec» := leading_parser:leadPrec @[run_builtin_parser_attribute_hooks] def whereDecls := leading_parser - " where" >> sepBy1Indent (ppGroup letRecDecl) "; " (allowTrailingSep := true) + "where" >> sepBy1Indent (ppGroup letRecDecl) "; " (allowTrailingSep := true) @[run_builtin_parser_attribute_hooks] def matchAltsWhereDecls := leading_parser diff --git a/tests/lean/formatTerm.lean b/tests/lean/formatTerm.lean index d4a8185855..1500e469b4 100644 --- a/tests/lean/formatTerm.lean +++ b/tests/lean/formatTerm.lean @@ -52,3 +52,10 @@ set_option format.indent 4 in #eval fmt `(let x := { foo := bar bar := foo + bar } x) + +#eval fmt `(command| +def foo : a b c d e f g a b c d e f g h where + h := 42 + i := 42 + j := 42 + k := 42) diff --git a/tests/lean/formatTerm.lean.expected.out b/tests/lean/formatTerm.lean.expected.out index c5e4c7c56f..70ede97f22 100644 --- a/tests/lean/formatTerm.lean.expected.out +++ b/tests/lean/formatTerm.lean.expected.out @@ -61,3 +61,9 @@ let x✝ := { foo✝ := bar✝ bar✝ := foo✝ + bar✝ } x✝ +def foo✝ : a✝ b✝ c✝ d✝ e✝ f✝ g✝ a✝ b✝ c✝ d✝ e✝ f✝ g✝ h✝ + where + h✝ := 42 + i✝ := 42 + j✝ := 42 + k✝ := 42