*To*: Andrew Gacek <andrew.gacek at gmail.com>*Subject*: Re: [isabelle] No warning for non-exhaustive case*From*: Dmitriy Traytel <traytel at in.tum.de>*Date*: Wed, 10 Jun 2015 08:25:54 +0200*Cc*: isabelle-users <isabelle-users at cl.cam.ac.uk>*In-reply-to*: <CAHgzvFh1EwrBqjq+3YK2_PhCqW+=uRQVM=XUqoOECejCi-9UoQ@mail.gmail.com>*References*: <CAHgzvFgu0hKnp9HhQbqrJSaV1zEaupLXd3JH4G5gwZTK9Duscw@mail.gmail.com> <55775F16.7060604@in.tum.de> <CAHgzvFh1EwrBqjq+3YK2_PhCqW+=uRQVM=XUqoOECejCi-9UoQ@mail.gmail.com>*User-agent*: Mozilla/5.0 (X11; Linux x86_64; rv:31.0) Gecko/20100101 Thunderbird/31.7.0

Hi Andrew,

Dmitriy 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. -Andrew On Tue, Jun 9, 2015 at 4:48 PM, Dmitriy Traytel <traytel at in.tum.de> 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 â Context.>> (Syntax_Phases.term_check 2 "Warn undefined" (fn _ => fn ts => let 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)) â Dmitriy 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 warning: fun f :: "nat => nat" where "f x = (case x of 0 => 0)" Thanks, Andrew

**References**:**[isabelle] No warning for non-exhaustive case***From:*Andrew Gacek

**Re: [isabelle] No warning for non-exhaustive case***From:*Dmitriy Traytel

**Re: [isabelle] No warning for non-exhaustive case***From:*Andrew Gacek

- Previous by Date: [isabelle] Synchronisation of thm, find_theorems, etc.
- Next by Date: Re: [isabelle] Splicing runtime ML values into Isar
- Previous by Thread: Re: [isabelle] No warning for non-exhaustive case
- Next by Thread: [isabelle] Splicing runtime ML values into Isar
- Cl-isabelle-users June 2015 archives indexes sorted by: [ thread ] [ subject ] [ author ] [ date ]
- Cl-isabelle-users list archive Table of Contents
- More information about the Cl-isabelle-users mailing list