[isabelle-dev] Type variables without default sort

2011-06-29 Thread Lars Noschinski
Hi all, every once in a while, I manage to create a goal state which contains type variables with the empty sort (for example in f x = 0, x is of type 'b :: {}, if there are no additional constraints on f. Some tools don't like this (e.g. metis omits a warning, SMT fails altogether) and it

Re: [isabelle-dev] Type variables without default sort

2011-06-29 Thread Makarius
On Wed, 29 Jun 2011, Lars Noschinski wrote: every once in a while, I manage to create a goal state which contains type variables with the empty sort (for example in f x = 0, x is of type 'b :: {}, if there are no additional constraints on f. Some tools don't like this (e.g. metis omits a

Re: [isabelle-dev] Type variables without default sort

2011-06-29 Thread Tobias Nipkow
Yes, it is a problem of unintended generality. The question remains: are there known situations where it is intended, or could one restrict the generated type variables in the same way as the explicitly stated ones. Tobias Am 29/06/2011 17:23, schrieb Makarius: On Wed, 29 Jun 2011, Lars