Does the current attribute mechanism support selective attributes such
as [code_inline cong], maybe along the lines of [simp del]? If it does,
I assume it would be easy to add that information in the place that
Florian pointed to?
Tobias
Am 28/05/2011 14:45, schrieb Florian Haftmann:
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.
http://isabelle.in.tum.de/reports/Isabelle/file/0f9534b7ea75/src/Tools/Code/code_preproc.ML#l10.
Maybe it would be worth thinking about transfering all simpset
declaration attributes also to code_inline.
Hope this helps,
Florian
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
