Stream: Beginner Questions

Topic: Can I use a locale to define a language?

david streader (Nov 27 2021 at 19:38):

Hi
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?

Lukas Stevens (Nov 28 2021 at 12:39):

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: Apr 19 2024 at 16:20 UTC