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



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






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