feat(src/frontends/lean/pp): look at pp.proofs when pp-ing coercions

src/frontends/lean/pp.cpp

@@ -387,7 +387,10 @@ bool pretty_fn::is_prop(expr const & e) {
 
 auto pretty_fn::pp_coercion_fn(expr const & e, unsigned sz, bool ignore_hide) -> result {
     if (sz == 1) {
-        return pp_child(app_arg(e), max_bp()-1, ignore_hide);
+        expr arg = app_arg(e);
+        if (auto thm = arg_is_proof(app_fn(e)))
+            arg = mk_inaccessible(*thm);
+        return pp_child(arg, max_bp()-1, ignore_hide);
     } else if (is_app(e) && is_implicit(app_fn(e))) {
         return pp_coercion_fn(app_fn(e), sz-1, ignore_hide);
     } else {
@@ -396,7 +399,10 @@ auto pretty_fn::pp_coercion_fn(expr const & e, unsigned sz, bool ignore_hide) ->
         format fn_fmt   = res_fn.fmt();
         if (m_implict && sz == 2 && has_implicit_args(fn))
             fn_fmt = compose(*g_explicit_fmt, fn_fmt);
-        result res_arg  = pp_child(app_arg(e), max_bp(), ignore_hide);
+        expr arg = app_arg(e);
+        if (auto thm = arg_is_proof(fn))
+            arg = mk_inaccessible(*thm);
+        result res_arg  = pp_child(arg, max_bp(), ignore_hide);
         return result(max_bp()-1, group(compose(fn_fmt, nest(m_indent, compose(line(), res_arg.fmt())))));
     }
 }
@@ -554,10 +560,10 @@ auto pretty_fn::pp_child(expr const & e, unsigned bp, bool ignore_hide) -> resul
             return pp_abbreviation(e, *it, true, bp, ignore_hide);
         } else if (is_implicit(f)) {
             return pp_child(f, bp, ignore_hide);
-        } else if (auto thm = arg_is_proof(f)) {
-            return pp_child_core(mk_app(f, mk_inaccessible(*thm)), bp, ignore_hide);
         } else if (!m_coercion && is_coercion(m_env, get_app_fn(e))) {
             return pp_coercion(e, bp, ignore_hide);
+        } else if (auto thm = arg_is_proof(f)) {
+            return pp_child_core(mk_app(f, mk_inaccessible(*thm)), bp, ignore_hide);
         }
     }
     return pp_child_core(e, bp, ignore_hide);

tests/lean/pp_proofs_coercions.lean

@@ -0,0 +1,18 @@
+constants (A : Type) (B : A → Type) (C : Π a, B a → Type)
+constants (f : Π a b, C a b → (true → true))
+attribute f [coercion]
+
+print coercions
+
+constants (a : A) (b : B a) (c : C a b)
+
+definition messy₁ := f a b c
+definition messy₂ := f a b c trivial
+
+eval messy₁
+eval messy₂
+
+set_option pp.proofs false
+
+eval messy₁
+eval messy₂

tests/lean/pp_proofs_coercions.lean.expected.out

@@ -0,0 +1,6 @@
+C ↣ _Fun : f
+C ↣ [fun-class] : f
+c
+c trivial
+c
+c ⌞true⌟