Hi Jasmin,
There will be a high level of compatibility between the old and the
new package.
For nonnested recursive datatypes, compatibility is quasi-100%; and for nested
datatypes, the package will support an optional nested to mutual reduction
to
simulate the old package, so that the same
Hi Jasmin,
What is the proper technical term for that? Isn't it just corec?
If the proper name for primrec is primrec, then the proper name for this
is primcorec.
I wouldn't mind killing the prim -- after all, the recursor constants are
just called _rec -- but that's an orthogonal
Hi Josh,
QUESTION STATED BRIEFLY:
If I convert existing proofs in src/HOL/**.thy from apply-style to
Isar-style, would those changes be welcome in the main repository?
beyond the general hints given by Makarius, you could go the following way:
a) Find a nice example (section) in theories
Am 04.08.2013 18:57, schrieb Florian Haftmann:
For nonnested recursive datatypes, compatibility is quasi-100%; and for nested
datatypes, the package will support an optional nested to mutual reduction to
simulate the old package, so that the same theorems as before are available
(albeit under
On 08/04/2013 07:09 PM, Florian Haftmann wrote:
To add a further dimension to the design space, there was once the idea
of a generalized primrec in the manner:
1. recursive specification following some pattern considered »primitive«
2. foundational definition of this specification using a
Hi isabelle-dev,
Makrius should know already, but I think it is a good idea to inform everyone
here that a current student's project is about to provide a bit more advanced
user interface for the find theorems functionality. It should be finished in
two weeks time.
Fabian
There is also a more technical reason why we want to perform the nested
to mutual reduction: It gives us a very cheap compatibility layer for
the old package. I.e. everything that is defined by the new package and
falls into the fragment of the old package can be registered as an old
datatype
On Sunday, August 4, 2013 at 20:32:50 (+0200), Dmitriy Traytel wrote:
I.e. everything that is defined by the new package and
falls into the fragment of the old package can be registered as an old
datatype benefiting from all the infrastructure built around it (e.g.
size function,
Hi Florian,
Am 04.08.2013 um 18:57 schrieb Florian Haftmann
florian.haftm...@informatik.tu-muenchen.de:
has an explicit need for a »nested to mutual« mode ever been
articulated?
Yes, on a couple of occasions. First, as Dmitriy mentioned, compatibility is
important -- I certainly don't want
