From 3a9cfeb9fb02017bda77c1e9b1f06eb179f116af Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sun, 30 Aug 2020 08:37:51 -0700 Subject: [PATCH] fix: `lookahead.formatter` --- src/Lean/PrettyPrinter/Formatter.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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 :=