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).

Tobias

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
logic?)

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,

Thomas






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