Stream: Isabelle/ML

Topic: Exception in COMP

view this post on Zulip Lukas Stevens (Aug 24 2021 at 13:21):

Any ideas what causes this exception?

exception THM 1 raised (line 700 of "drule.ML"):
  COMP
  S :000 :001  [S :000 :001]
  ?r ?a ?b ⟹ ?r⇧+⇧+ ?a ?b

view this post on Zulip Lukas Stevens (Aug 24 2021 at 14:28):

The problem is that there are multiple unifiers. I am not yet sure how to fix it.

view this post on Zulip Manuel Eberl (Aug 24 2021 at 19:53):

Hmm. Is first-order matching enough for you, perhaps? Otherwise you could try instantiating things manually.

Last updated: Apr 19 2024 at 04:17 UTC