Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] ML Error Message When using Number_Theory (Isa...

view this post on Zulip Email Gateway (Aug 22 2022 at 16:35):

From: Kremann Tim <twkrema@tycho.ncsc.mil>
When attempting to use Number_Theory, I am getting the following error message:

ML Warning (line 50 of “~~/src/HOL/Library/Cancellation/cancel.ML”):
Pattern is not exhaustive.
signature CANCEL = sig al proc: Proof.context -> cterm -> thm option end
functor Cancel_Fun (Data: CANCEL_NUMBERS_DATA): CANCEL

Is there a fix for this?

Tim Kremann
twkrema@tycho.ncsc.mil

view this post on Zulip Email Gateway (Aug 22 2022 at 16:35):

From: Lars Hupel <hupel@in.tum.de>
Dear Tim,

I'm assuming you're referring to the yellow-ish message you get in
"Cancellation.thy". This is not an error, but a warning. Warnings from
Isabelle that appear in the Isabelle distribution can be safely ignored
by users.

Cheers
Lars

Last updated: Apr 19 2024 at 08:19 UTC