Re: [isabelle] Warning for partial functions defined with fun?

Dear Thomas,

The development version does now give you warnings about missing cases (thanks to your suggestion when you visited).


Am 23/06/2011 12:13, schrieb Thomas Genet:

Dear Isabelle users,

I am planning to use Isabelle to teach "formally verified programming"
to developpers...
I am going to use the "fun" construction for defining recursive
functions. (Unless I make a mistake the "function" construction is too
verbose, and maybe too complex, for regular developpers not so found of

However, I am a bit confused with this construction since it does not
compain (or at least warn the user) with partial functions... though
when programming in Ocaml (for instance) such warning are common.

Is there a simple solution to switch on such messages?

Thanks in advance,


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