Stream: Beginner Questions

Topic: ✔ Failed to apply proof method


view this post on Zulip Robert Soeldner (Sep 02 2021 at 17:55):

Is there any way to get more information, why a proof method is not applicable?
I'm currently facing the following goal:
1. ⟦wf_graph G; wf_rule r; wf_cat CatGraph; dang r G m⟧ ⟹ ∃p. wf_pushout CatGraph p m m and I'm able to apply the following introduction rule
apply (rule exI[where x = "⦇pf' = (undefined, m, undefined), pg' = (undefined, m, undefined)⦈"]) but as soon as I start to replace one undefined with for example G I get Failed to apply proof method⌂:.

view this post on Zulip Robert Soeldner (Sep 02 2021 at 18:45):

Found it, using [[unify_trace_failure]]
Still difficult for me to find these. Any reason they are not listed in the isar-ref PDF?

view this post on Zulip Notification Bot (Sep 04 2021 at 16:51):

Robert Soeldner has marked this topic as resolved.


Last updated: Sep 25 2022 at 23:25 UTC