Zulip Chat Archive

Stream: new members

Topic: debugging tactics


view this post on Zulip 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 [] [],
  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?

view this post on Zulip Alex J. Best (Oct 15 2020 at 22:29):

You can trace the output:

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

view this post on Zulip Kevin Lacker (Oct 15 2020 at 22:30):

perfect, exactly what i wanted


Last updated: May 10 2021 at 17:39 UTC