On 08/31/2011 04:21 PM, Andreas Schropp wrote:
On 08/30/2011 08:12 PM, Brian Huffman wrote:
However, the nonemptiness proof does rely on type class assumptions:
Indeed, "{A. ~ finite A}" is actually empty for any finite type 'a.
I think I get your point now: assumptions for type class constraints
on variables are indeed local to nonemptiness-proofs if we eliminate
typeclass-reasoning and don't regard it as primitive.
Generalizing the type well-formedness arguments to depend on arbitrary
local assumptions (instead of only type class assumptions) is the treatment
of local typedefs I talked about earlier.
But I think your suggestion via a different semantic interpretation of
typedefs would result in easier code.
Cheers,
Andy
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
