See now 8b7508f848ef. Library/Lattice_Constructions contains the remains of
Library/Quickcheck_Types.
Andreas
On 18/08/14 18:44, Peter Lammich wrote:
However, the constructions might still be useful, as the following comment from
Peter
Lammich's AFP entry Refine_Monadic shows.
(* TODO:
On 15/08/2014 09:30, Andreas Lochbihler wrote:
In 51aa30c9ee4e, I have added lattice instances for the Enum.finite_* types.
As
expected, this suffices for the quickcheck examples in
Quickcheck_Lattice_Examples (see 9225b2761126).
This now raises the question what we should do with
In 51aa30c9ee4e, I have added lattice instances for the Enum.finite_* types. As expected,
this suffices for the quickcheck examples in Quickcheck_Lattice_Examples (see 9225b2761126).
This now raises the question what we should do with HOL/Library/Quickcheck_Types. Within
the Isabelle
I’m afraid that I don’t even know what it is.
Larry
On 11 Jul 2014, at 12:21, Florian Haftmann
florian.haftm...@informatik.tu-muenchen.de wrote:
The issue that src/HOL/Library/Quickcheck_Types.thy is dead and broken
has not been addressed since before the last release.
So, which path to
On Fri, 11 Jul 2014, Andreas Lochbihler wrote:
If there's consensus on reviving this theory, I can do the changes to
Quickcheck_Types such that Isabelle2014 digests it. This is probably all
that can be done before the release as most of us will be busy in Vienna
next week. A move to Main is
Quickcheck does not use these types, because it is currently configures to only use the
types finite_1 to finite_3 from Enum, because the finite_types parameter is set by
default. Quickcheck internally also seems to work differently depending on whether the
finite_types flag is set.
I have
Te discussion has faded out here a few months ago.
Again, shall we attempt a serious repair effort?
Florian
--
PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de
signature.asc
Description: OpenPGP digital signature
