From f64784378a4745e1da174ea4014be36d429f9fe2 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Wed, 10 Jun 2015 16:19:27 -0700 Subject: [PATCH] fix(frontends/lean/pp): make pp_have more robust We should not assume the argument of a have_annotation is a lambda. --- src/frontends/lean/pp.cpp | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/src/frontends/lean/pp.cpp b/src/frontends/lean/pp.cpp index 9fa6ba52b3..1463d0b5d9 100644 --- a/src/frontends/lean/pp.cpp +++ b/src/frontends/lean/pp.cpp @@ -730,7 +730,9 @@ auto pretty_fn::pp_pi(expr const & e) -> result { } } -static bool is_have(expr const & e) { return is_app(e) && is_have_annotation(app_fn(e)); } +static bool is_have(expr const & e) { + return is_app(e) && is_have_annotation(app_fn(e)) && is_binding(get_annotation_arg(app_fn(e))); +} static bool is_show(expr const & e) { return is_show_annotation(e) && is_app(get_annotation_arg(e)) && is_lambda(app_fn(get_annotation_arg(e)));