[isabelle] Warning for partial functions defined with fun?
- To: isabelle-users at cl.cam.ac.uk
- Subject: [isabelle] Warning for partial functions defined with fun?
- From: Thomas Genet <Thomas.Genet at irisa.fr>
- Date: Thu, 23 Jun 2011 12:13:48 +0200
- User-agent: Mozilla/5.0 (Macintosh; U; Intel Mac OS X 10.5; fr; rv:184.108.40.206) Gecko/20110616 Thunderbird/3.1.11
Dear Isabelle users,
I am planning to use Isabelle to teach "formally verified programming"
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,
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