Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] conditional equations and code generation

Email Gateway (Aug 18 2022 at 18:28):

From: Christian Sternagel <christian.sternagel@uibk.ac.at>
Hi all,

In isabelle doc functions it is correctly stated that code generation
does not handle conditional equations. Just for fun I tried it anyway
and found it a bit strange to not get an error (instead the code does
just not contain the conditional equation). I think raising an error
would be more appropriate. What do you think?

cheers

chris

Email Gateway (Aug 18 2022 at 18:29):

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

the policy of default code equations is to be ignored silently if they
are not syntactically suitable. With explicit declarations

declare f.simps [code]

you will get an error.

This behaviour avoids verbose warnings.

Florian
signature.asc

Last updated: Nov 21 2024 at 12:39 UTC