Re: [isabelle] Code generation with type classes leads to compile error

Hi Dominique,

> However, by try and error I managed to find a hack for my specific case:
> lemma [code]: "(uniformity :: ('a ell2 * _) filter) =
> Filter.abstract_filter (%_.
>     Code.abort STR ''no uniformity'' (%_.
>     let x = ((=)::'a⇒_⇒_) in uniformity))"

that is more or less all you can do at the moment.

There has been a thread on the dev mailing list dealing with the issue
which AFAIKS came to the same conclusion.


Attachment: signature.asc
Description: OpenPGP digital signature

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