Previously I have used a locale to define Galois connections different ways so they are not completely unknown to me. But I am trying to define one language ZOL (propositional logic) as a sub language to another language FOL and not getting very far!
Slowly moving forward but I have been using value " power .... " to debug my power functions. This works outside of the local but when the functions and value are in a locale I get "No code equations for local.power"
Any ideas what I am doing wrong?
Defining functions inside a locale has the unfortunate side effect that the equations of the function then depend on the locale assumptions. Since the code generator cannot deal with conditional equations you will see the error you mentioned when using
value. The remedy is to define functions outside the locale. If the locale depends on some constants that you want to use inside the function, you can use an anonymous context that resembles the locale to make the function easier to define. Example:
locale foo = fixes a :: 'a begin end context fixes a :: 'a begin fun f where "f x = a" end
Last updated: Jun 06 2023 at 23:15 UTC