debugging tactics

Stream: new members

[Kevin Lacker]

I want to call a noninteractive tactic at a particular point in a program, just to see what its output is. Something like this:

import data.nat.basic
import tactic.solve_by_elim

lemma bar (n : ℕ) (h1 : 0 < n) : 0 < n ^ 2 :=
begin
  let x := tactic.solve_by_elim.mk_assumption_set ff [] [],
  admit
end

My idea was, and then try to figure out what x is. But, I can't do that, it errors with "invalid definition, it uses untrusted declaration 'tactic'". Is there a way I can do this?

[Alex J. Best]

You can trace the output:

  trace (tactic.solve_by_elim.mk_assumption_set ff [] []),

[Kevin Lacker]

perfect, exactly what i wanted