diff --git a/src/Lean/PrettyPrinter/Formatter.lean b/src/Lean/PrettyPrinter/Formatter.lean index 32c8e38e23..5def533fdb 100644 --- a/src/Lean/PrettyPrinter/Formatter.lean +++ b/src/Lean/PrettyPrinter/Formatter.lean @@ -230,7 +230,7 @@ p @[combinatorFormatter Lean.Parser.lookahead] def lookahead.formatter (p : Formatter) : Formatter := -p +pure () @[combinatorFormatter Lean.Parser.andthen] def andthen.formatter (p1 p2 : Formatter) : Formatter :=