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.

view this post on Zulip Notification Bot (May 13 2022 at 08:36):

Robert Soeldner has marked this topic as resolved.

Last updated: Nov 05 2025 at 20:25 UTC