[isabelle] No warning for non-exhaustive case



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.