From a02c6e70fa4f110f5c9c9997a35cc4a1457d3c2d Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 27 Dec 2013 12:13:36 -0800 Subject: [PATCH] fix(frontends/lean/pp): missing parenthesis around nested forall/exists Signed-off-by: Leonardo de Moura --- src/frontends/lean/pp.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/frontends/lean/pp.cpp b/src/frontends/lean/pp.cpp index 37c667ee65..bedad0c7ff 100644 --- a/src/frontends/lean/pp.cpp +++ b/src/frontends/lean/pp.cpp @@ -436,7 +436,7 @@ class pp_fn { return g_eq_precedence; } else if (is_arrow(e)) { return g_arrow_precedence; - } else if (is_lambda(e) || is_pi(e) || is_let(e)) { + } else if (is_lambda(e) || is_pi(e) || is_let(e) || is_forall(e) || is_exists(e)) { return 0; } else { return g_app_precedence;