Stream: General

Topic: Enter Match Example

view this post on Zulip Fabian Huch (Feb 26 2024 at 14:03):

Does anyone have a small example where the infamous ENTER MATCH message is triggered?

view this post on Zulip Manuel Eberl (Feb 27 2024 at 12:27):

From the mailing list:

theory SimpleStuff imports Main
begin
 typedecl i
 consts a::i b::i

 axiomatization where
  A1: "¬(a = b)" and
  A2: "∀x::i. x = a ∨ x = b"

 theorem T1: "∃(F::(i⇒bool)⇒i). ∀T::i. (∃(S::i⇒bool). F S = T)"
   apply fastforce

view this post on Zulip Manuel Eberl (Feb 27 2024 at 12:38):

meme.jpg

view this post on Zulip Fabian Huch (Feb 27 2024 at 13:14):

Turns out that fastforce just finds the proof when you prevent it from printing...

Last updated: May 02 2024 at 01:06 UTC