On Wed, 27 Feb 2013, Tobias Nipkow wrote:
All known incidents were of the category as the present one: someone
who is not yet conditioned to watch out for excess polymorphism
stumbles over it, and gets surprised how ond type parameters here
suddenly shows up there. But this can be avoided by
In Edinburgh LCF, term quotations containing anonymous type variables were
simply rejected. Perhaps that would still be the best approach now. I'm not
convinced that it would lead to more errors than the 'a itself approach.
Larry
On 1 Mar 2013, at 11:35, Makarius makar...@sketis.net wrote:
I
On Fri, 1 Mar 2013, Lawrence Paulson wrote:
In Edinburgh LCF, term quotations containing anonymous type variables
were simply rejected. Perhaps that would still be the best approach now.
I'm not convinced that it would lead to more errors than the 'a itself
approach.
I know, you've
Some more hints at the general perspective of variants of Hindley-Milner
polymorphism:
* Many Java programmers consider type-inference a bug.
* Scala people are used to a much more complex situation than in ML,
Haskell, or Isabelle.
Apart from Odersky himself there is probably nobody
Dear all,
in the repository (8a635bf2c86c) and in Isabelle2013, there seems to be
something wrong with the enat_eq_cancel simproc in Extended_Nat. Can
someone please look into this? Here's a minimal example:
theory Scratch imports
~~/src/HOL/Library/Extended_Nat
begin
definition epred ::
On 01.03.2013 15:10, Andreas Lochbihler wrote:
By the way, why does the failure in the simproc yield a proof error at
all? Usually, simp does not raise Proof failed if it gets stuck
somewhere.
I guess this means that the simproc raises Proof failed which merely
propagates through the
