Stream: Beginner Questions

Topic: Debug metis

view this post on Zulip Robert Soeldner (May 12 2022 at 13:53):

Is it possible to see how metis manages to finish a proof?
My current proof ends with:

    apply (auto simp add: fun_eq_iff morph_comp_def split: if_splits)
    apply metis
    by metis

And I would like to drop the two metis calls.

view this post on Zulip Maximilian Schaeffeler (May 13 2022 at 08:26):

There are metis_trace and metis_verbose, but I don't know how to read the output,
e.g. using [[metis_trace]] by metis.

Last updated: Jul 15 2022 at 23:21 UTC