Email Gateway (Aug 18 2022 at 17:49): Email Gateway (Aug 18 2022 at 17:49):From: Thomas Genet <Thomas.Genet@irisa.fr>
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
Email Gateway (Aug 18 2022 at 17:49):From: Tobias Nipkow <nipkow@in.tum.de>
Dear Thomas,
The development version does now give you warnings about missing cases
(thanks to your suggestion when you visited).
Tobias
Email Gateway (Aug 18 2022 at 17:49):From: Thomas Genet <Thomas.Genet@irisa.fr>
Dear Tobias,
great! I remember about this discussion but did not imagine that it was
already added to Isabelle :-)
Do you know if I can apply a particular changeset to my Isabelle2011 or
have to get the full developpement version?
Thanks in advance,
Thomas
Email Gateway (Aug 18 2022 at 17:49):From: Alexander Krauss <krauss@in.tum.de>
Hi Thomas,
great! I remember about this discussion but did not imagine that it was
already added to Isabelle :-)
The relevant changeset is here:
http://isabelle.in.tum.de/repos/isabelle/rev/fcb6250bf6b4
Do you know if I can apply a particular changeset to my Isabelle2011 or
have to get the full developpement version?
This one is simple enough, and there haven't been much changes, so it
should probably work if you just apply this change (click on "raw" at
the URL above to get the actual patch) and recompile HOL using "./build".
In general, this almost never works, due to interactions with other
changes, but here you may be lucky.
Alex
Last updated: Apr 19 2024 at 12:27 UTC