On 04/18/2012 08:26 PM, Florian Haftmann wrote:
Hi all,
- I would like to add a size limit to records beyond which no code generator setup
is performed. The main reason is that on sizes 200 fields or so, the setup
does not make any sense, but consumes very large amounts of memory (and
On Thu, 19 Apr 2012, Gerwin Klein wrote:
Btw, it's easy to reproduce: just make a theory file based on HOL
(Main.thy) that defines a record with 600 fields. Run it in
Isabelle-2009-1 and the current version for comparison.
We also have a semi-active src/HOL/Record_Benchmark for quite some
Currently, the sort of a type variable in a type is constrained by attaching
::S to it. Right in the middel of the type, eg 'a::ord = 'a = bool. This
can make types less readable. In Haskell this is expressed with a separate
context. After some discussion in Munich we propose to support some such
This sounds like a good idea. The old notation was pretty unreadable.
Larry
On 19 Apr 2012, at 12:11, Tobias Nipkow wrote:
Currently, the sort of a type variable in a type is constrained by attaching
::S to it. Right in the middel of the type, eg 'a::ord = 'a = bool. This
can make types less
On Thu, 19 Apr 2012, Tobias Nipkow wrote:
Reactions?
Postpone discussion until after official rollout of Isabelle2012.
There still many things to be sorted out.
Makarius
___
isabelle-dev mailing list
isabelle-...@in.tum.de
I did not propose to add this before the release, but I don't see any harm in
discussing it now. In fact, now people may be more alert than later. Of course
you are welcome to add your two cents later.
Tobias
Am 19/04/2012 13:25, schrieb Makarius:
On Thu, 19 Apr 2012, Tobias Nipkow wrote:
On Thu, 19 Apr 2012, Tobias Nipkow wrote:
I did not propose to add this before the release, but I don't see any
harm in discussing it now. In fact, now people may be more alert than
later. Of course you are welcome to add your two cents later.
I do see a harm. A release is not a trivial
As I said: add them later.
Tobias
Am 19/04/2012 14:09, schrieb Makarius:
On Thu, 19 Apr 2012, Tobias Nipkow wrote:
I did not propose to add this before the release, but I don't see any harm in
discussing it now. In fact, now people may be more alert than later. Of
course
you are welcome
On Tue, 10 Apr 2012, Brian Huffman wrote:
On Tue, Apr 10, 2012 at 3:06 PM, Makarius makar...@sketis.net wrote:
Isabelle/a380515ed7e4 and AFP/53124641c94b produce the following error:
*** No code equations for one_word_inst.one_word
*** At command by (line 174 of
On Thu, Apr 19, 2012 at 4:02 PM, Makarius makar...@sketis.net wrote:
On Tue, 10 Apr 2012, Brian Huffman wrote:
On Tue, Apr 10, 2012 at 3:06 PM, Makarius makar...@sketis.net wrote:
Isabelle/a380515ed7e4 and AFP/53124641c94b produce the following error:
*** No code equations for
Hi Florian,
I understood that much. What I was hoping for was an answer on a more
technical level. The definition + interpretation pattern seem a
useful thing to have. But it sounds like, if you change the main
interpretation command like this, you will break it for intended use
cases
On Thu, 19 Apr 2012, Clemens Ballarin wrote:
Maybe what you want is an alternative command to 'interpretation'.
Creating definitions from definition to me is not interpreting something
in some other context by means of existing entities, but creating a new
instance of something. The
12 matches
Mail list logo
