I have two items of interest for the coming release.
There is some interest here at Data61 (NICTA that was) in having a
localised record package in Isabelle-2016. I've done the initial
implementation and got the parts of the package I understand working
within locales etc, but something goes wron
As Andreas and Lars have pointed out, this is the issue described in
§7.1 in the tutorial on code generation.
I will have a look at this after the release.
Florian
Am 12.01.2016 um 23:51 schrieb Makarius:
> On Tue, 12 Jan 2016, Manuel Eberl wrote:
>
>> I commented out the code equation
Hi all,
> This is probably a question for Florian. I introduced Euclidean rings to
> allow a more systematic derivation of (constructive) GCDs about two
> years ago or so.
>
> Since then, Florian cleaned this up and improved it a lot, but from what
> I gathered, there is much to be done yet. I sh
Hi Thomas,
> There is some interest here at Data61 (NICTA that was) in having a
> localised record package in Isabelle-2016. I've done the initial
> implementation and got the parts of the package I understand working
> within locales etc, but something goes wrong with the code generation
> aspect
Dear all,
>
> I have already some post-release patches in the pipeline which would add
> this instance anyway. So, there is no demand for action here at the moment.
>
> Note that the classes (semi)ring_gcd in Isabelle2015 had no lemmas and
> thus very hardly different from syntactic classes, so
Hi Rene,
>> Note that the classes (semi)ring_gcd in Isabelle2015 had no lemmas and
>> thus very hardly different from syntactic classes, so there is no loss
>> of generality here.
>
> I disagree with this second item: the classes (semi)ring_gcd in Isabelle2015
> have
> the three essential lemmas
Hi Johannes, hi Andreas,
the core of the problem is that dictionaries are always generated for
type class instances, even if the operations therein are never referred
to. Is this the first time that we have such a situation, or are there
more examples (e.g. in the AFP)? If yes, the code generato
On Thu, 14 Jan 2016, Thomas Sewell wrote:
The second proposal is probably more contentious. I'm hoping to
reimplement a tool we had in the past that speeds up proof maintenance
work by selectively skipping proofs that are very likely to succeed. To
support that, I'm proposing adding a couple o
On Thu, 14 Jan 2016, Florian Haftmann wrote:
Hi Thomas,
There is some interest here at Data61 (NICTA that was) in having a
localised record package in Isabelle-2016. I've done the initial
implementation and got the parts of the package I understand working
within locales etc, but something goe
On Thu, 14 Jan 2016, Thomas Sewell wrote:
Right. There was a plan here to investigate before the release, but the
timing didn't work out.
You mean *after* the release. Bigger changes are always reconsidered
after lift-off of release N, to be included in release N + 1 or N + k for
k >= 2.
On Thu, 14 Jan 2016, Florian Haftmann wrote:
Note that the classes (semi)ring_gcd in Isabelle2015 had no lemmas and
thus very hardly different from syntactic classes, so there is no loss
of generality here.
I disagree with this second item: the classes (semi)ring_gcd in Isabelle2015
have
the
This is an update on the situation: after the informal Isabelle2016-RC0
and many additions and clarifications, we are moving towards the first
formal Isabelle2016-RC1.
This will happen in a few days on the main isabelle-dev repository,
without a fork yet. Thus it is easier to finish remaining
AFAIK, it is the first time we have such a situation. We have two cases
I'm aware of: "open" in topological_space and "uniformity" in
uniform_space. Up to now we could just remove all code equations from
open as it is a predicate and doesn't produce any problem with the
dictionary construction.
Yo
13 matches
Mail list logo
