Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] list_to_set_comprehension bug ?

Email Gateway (Aug 18 2022 at 16:47):

From: Mathieu Giorgino <mathieu.giorgino@irit.fr>
Hello all,

It seems there is a problem with the list_to_set_comprehension tactic for
terms containing a pattern matching on a datatype with a single constructor
with at least three arguments (It appears as a rather specific problem...).

datatype t = T unit unit unit

(* declare [[ simproc del: list_to_set_comprehension ]] *)

lemma "set (case n of T a b c ⇒ [b]) ≠ {}"
by (auto split:t.splits) (* *** Tactic failed *)

Is this a bug ?

Regards,

Mathieu

Email Gateway (Aug 18 2022 at 16:48):

From: Makarius <makarius@sketis.net>
Since this refers to an unofficial Isabelle version, it should be
discussed on the isabelle-dev@in.tum.de mailing list.

Makarius

Last updated: Nov 21 2024 at 12:39 UTC