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
https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/2016-January/006552.html
which AFAIKS came to the same conclusion.

Cheers,
	Florian

Attachment: signature.asc
Description: OpenPGP digital signature



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