It does not work for any datatype (for example as soon as a non-countable type
is used in the datatype) but it could be integrated in the datatype package
with some checks.
However, I don't know if the time penalty (which isn't so big but there
anyway) on a so much used feature worth the benefi
Hi all,
I have written a little ML library allowing to automatically prove, in most
cases, instantiations of types (typedefs, records and datatypes) as countable
(see ~~/src/HOL/Library/Countable). The style of the library is still a little
rough but I think it could be a nice addition to the I
Actually, there is a third code generator hidden somewhere in Isabelle.
- Steven
On 21.07.2011, at 12:18, Lukas Bulwahn wrote:
> Hello all,
>
>
> at the moment, we have two code generators in Isabelle:
>
> 1. An ancient code generator in Isabelle by Stefan Berghofer - limited to SML
> withou
Lukas already assured me of that. No worries here.
- Steven
On 22.07.2011, at 00:07, Alexander Krauss wrote:
> On 07/21/2011 04:25 PM, Steven Obua wrote:
>> Actually, there is a third code generator hidden somewhere in
>> Isabelle.
>
> If you are talking about what I know under the name "Comput
On 07/21/2011 04:25 PM, Steven Obua wrote:
Actually, there is a third code generator hidden somewhere in
Isabelle.
If you are talking about what I know under the name "Compute Oracle",
then rest assured that it is hidden well enough that the chance of some
user accidentially confusing it with
Hello everyone,
Attached is an implementation of a "countable_typedef" method that I
just wrote. (It works in a very similar manner to the
"countable_datatype" method.) Since records are implemented as
typedefs of product types, the same method works for record types as
well. I'd be happy to add t
On 07/21/2011 09:47 PM, Gerwin Klein wrote:
The idea has potential for generalisation. Could we turn this into
something similar to Haskell's "deriving"?
The command would take a datatype and a list of instantiation methods
that each know how to instantiate a datatype for a specific type
class,
On 21/07/2011, at 8:15 PM, Alexander Krauss wrote:
> It comes in the form of a method, so it has to be invoked explicitly, but
> like this it doesn't produce any penalty when it is not used.
A separate command like this method looks like the right way to do such things.
The idea has potential f
Hi Matthieu,
I have written a little ML library allowing to automatically prove, in most
cases, instantiations of types (typedefs, records and datatypes) as countable
(see ~~/src/HOL/Library/Countable).
It seems that for datatypes we now have such functionality, implemented
four weeks ago by
This is definitely a useful tool for ImperativeHOL ... One could
probably integrate
it into the datatype package, such that datatypes automatically become
countable (like Haskell infers some typeclasses automatically (on demand))
Peter
Mathieu Giorgino schrieb:
Hi all,
I have written a littl
We moved recently to the new code-generator.
Burkhart
Am 21.07.2011 um 12:18 schrieb Lukas Bulwahn:
> Hello all,
>
>
> at the moment, we have two code generators in Isabelle:
>
> 1. An ancient code generator in Isabelle by Stefan Berghofer - limited to SML
> without supporting type classes.
Hello all,
at the moment, we have two code generators in Isabelle:
1. An ancient code generator in Isabelle by Stefan Berghofer - limited
to SML without supporting type classes.
Commands to invoke it were code_module and code_library.
2. A generic code generator in Isabelle by Florian Haftma
12 matches
Mail list logo
