## Stream: metaprogramming / tactics

### Topic: printing expr

#### Patrick Massot (Jan 24 2021 at 16:45):

I'm still desperately trying to get fully usable #5440 before my course starts but @Edward Ayers doesn't have time for this (he started his real world job). The code in the PR works great for display but the "copy to clipboard" button still has the default rendering of expr. In the PR, the quantifier collapsing code is deeply intertwined with the complicated annotated expressions needed for widgets. I'd like to reproduce the collapsing effect in a function from expr to tactic string. But I don't know how to print expression that actually feature de Bruijn indices. I made a small start with

import tactic

namespace tactic
setup_tactic_parser
open tactic

meta def collapsed_pp : expr → tactic string
| (expr.pi x xbi xy (expr.pi p pbi py b)) := do
pp_py ← tactic.pp py,
body ← collapsed_pp b,
pure ("∀ " ++ to_string pp_py ++ ", " ++ body)
| e := do pp_e ← pp e, pure pp_e.to_string

@[interactive]
meta def test (n : parse ident) : tactic unit :=
do e ← get_local n >>= infer_type,
s ← collapsed_pp e,
trace s,
skip

end tactic

example (h : ∀ n > 0, true) : true :=
begin
test h,
sorry
end


but the output is ∀ #0 > 0, true, which makes sense. How can I get my ∀ n > 0, true back by re-injecting the name x? Or should I do something else entirely? The global goal here is to go from e : expr to string which is a version of pp e where quantifiers are nicely collapsed as you can do on input.

#### Edward Ayers (Jan 24 2021 at 21:58):

Hi Patrick I'm having a look now dw :)

Pushed to #5440

#### Edward Ayers (Jan 24 2021 at 22:17):

There is a new method called pretty_print_with_collapsed_quantifiers that you can use

Last updated: May 09 2021 at 21:10 UTC