Re: [isabelle] Congruence rules for the code preprocessor

Hi Andreas,

> the code generator tutorial mentions that "the simpset for the code
> preprocessor can apply the full generality of the Isabelle simplifier".
> But how can I add anything else other than unfold theorems? The
> attributes code_unfold and code_inline do not accept declarations like
> declare conj_cong[code_inline cong]
> Is there a way in Isar to declare congruence rules to the preprocessor?

no, this can only be done on the ML level, cf.

Maybe it would be worth thinking about transfering all simpset
declaration attributes also to code_inline.

Hope this helps,



PGP available:

Attachment: signature.asc
Description: OpenPGP digital signature

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