Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Legacy feature warning in Nitpick

Email Gateway (Aug 22 2022 at 10:47):

From: Lars Hupel <hupel@in.tum.de>
Hi Jasmin,

I'm getting an odd warning when running Nitpick:

Nitpicking formula...
Legacy feature! Bad name binding: "…"
Legacy feature! Bad name binding: "…"
Nitpick found a counterexample:

Free variables:
t = Const s⇩1
u = Const s⇩1
Skolem constants:
??.matches.env = [s⇩1 ↦ Const s⇩1, … ↦ _]
??.matches.env = [s⇩1 ↦ Const s⇩1, … ↦ _]

I think I know what the output is trying to tell me (that there might be
other elements in the map, but we don't care), but I'm not sure where
the warning comes from. (In any case, the counterexample is correct.)

Cheers
Lars

Last updated: Apr 24 2024 at 12:33 UTC