interactive tactic printer

Stream: metaprogramming / tactics

[Xavier Martinet]

hi everyone,

is there anything like a tactic.pp for tactic.interactive ?

my use cases:

• when there is a "simp []", I would like to be able to print it as just "simp"
• when there is some open namespace, e.g, nat, I would like to be able to print expr in full names, e.g., "apply div" to be translated in "apply nat.div"

The only thing I have been able to do so far is this:

#eval do r ← lean.parser.run_with_input lean.parser.itactic_reflected "{ simp [] }", tactic.trace r.expr
/-
interactive.executor.execute_explicit tactic
  (has_bind.seq
     (has_bind.seq (tactic.save_info {line := 1, column := 0})
        (has_bind.seq
           (has_bind.seq (tactic.save_info {line := 1, column := 2})
              (tactic.istep 1 2 1 2
                 (tactic.interactive.simp none none ff list.nil list.nil (interactive.loc.ns [none]))))
           (tactic.save_info {line := 1, column := 11})))
     (tactic.save_info {line := 1, column := 10}))
-/

It seems to contain all the info needed, but maybe there is an off-the-shelf implementation?