Robert Soeldner (Sep 02 2021 at 17:55): 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⌂:.
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?
Notification Bot (Sep 04 2021 at 16:51):Robert Soeldner has marked this topic as resolved.
Last updated: Apr 19 2024 at 04:17 UTC