Re: [isabelle] Extra type variables, type classes and locales

Hallo Brian,

On Wed, Mar 4, 2009 at 4:35 PM, Brian Huffman <brianh at> wrote:
> [...]
> I would have expected the locale package to use the same trick to encode
> functions like your "test". That is, an extra hidden TYPE(?'a::testC)
> parameter should be added to make the type checker happy. I would consider
> this to be a bug in the locale implementation.
> By the way, the following definition *does* work inside the locale. Just
> like your inductive definition of "test", it uses type variable 'a on the
> right-hand side, but no type variable appears in the type of the constant.
> The only difference is that this one also uses the locale constant "dummy"
> on the right-hand side.
> [...]

Thanks for your answer. So I shouldn't count on there being a solution
to this problem apart from adding dummy variables into my definitions?
Well, it's not a big problem, it will probably just make some
definitions a bit less elegant.


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.