Re: [isabelle] No warning for non-exhaustive case

Hi Andrew,

please note that the code below is run on every term that is given to the type inference. And for the function package this is not only the term entered by the user, but also some internal stuff, where apparently undefined appears. I presume the command term and definition will not give warnings for "f x = (case x of 0 => 0 | Suc n => n)" (not tested).

Otherwise, you probably also want to emit a warning only when the undefined appears directly under a case combinator (this may reduce the number of false positives). Thus you will need to refine my rudimentary proposal.


On 10.06.2015 02:23, Andrew Gacek wrote:
Thanks, this does indeed catch the undefined. But for me it also gives
spurious warnings, e.g. on

fun f :: "nat => nat" where
   "f x = (case x of 0 => 0 | Suc n => n)"

This is on Isabelle2014.


On Tue, Jun 9, 2015 at 4:48 PM, Dmitriy Traytel <traytel at> wrote:
Hi Andrew,

no, there is no direct way to do this (i.e. the case translation facility
does not provide this functionality).

Of course, with Isabelle's user-space type inference, you can implement a
check phase that does what you want. Here is a quick and dirty example that
just shouts whenever it finds an undefined in a term (which is the case in
your example):

ML â
   (Syntax_Phases.term_check 2 "Warn undefined"
     (fn _ => fn ts =>
         val _ = map (fn t => fold_term_types (fn t => fn T => fn () =>
           if t = Const (@{const_name undefined}, T) then warning "undefined"
else ()) t ()) ts
       in ts end))


On 09.06.2015 22:44, Andrew Gacek wrote:
Is there a way to enable warnings when a case expression is
non-exhaustive? For example, Isabelle/HOL accepts this without a

fun f :: "nat => nat" where
    "f x = (case x of 0 => 0)"


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.