## Stream: new members

### Topic: debugging tactics

#### Kevin Lacker (Oct 15 2020 at 22:03):

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 [] [],
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 (Oct 15 2020 at 22:29):

You can trace the output:

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


#### Kevin Lacker (Oct 15 2020 at 22:30):

perfect, exactly what i wanted

Last updated: May 10 2021 at 17:39 UTC