Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Congruence rules for the code preprocessor

Email Gateway (Aug 18 2022 at 17:45):

From: Andreas Lochbihler <andreas.lochbihler@kit.edu>
Hi,

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?

Regards,
Andreas

Email Gateway (Aug 18 2022 at 17:46):

From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Andreas,

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
signature.asc

Last updated: Nov 21 2024 at 12:39 UTC