[isabelle] Warning for partial functions defined with fun?

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 Genet
Campus de Beaulieu, 35042 Rennes cedex, France
Tél: +33 (0) 2 99 84 73 44   E-mail: genet at irisa.fr

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