Re: [isabelle] finite sets and code generation, once again

Peter Gammie wrote:
> However it seems a bit limited: locale-fixed functions ("choice") are monomorphic, right? In other words, I would need to instantiate this locale at every type I wanted to apply "choice" to. I guess I'm asking for the locale equivalent of the polymorphic SOME.
Unfortunately, that is true. And we also have problems with this limitation.


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