Ant S. (Apr 09 2026 at 10:26): Ant S. (Apr 09 2026 at 10:26):theory test
imports Main
begin
locale test2
begin
datatype foo =
foo1 "foo list" | foo2 nat
value "foo1 ([(foo2 (2:: nat))] :: foo list)"
datatype bar =
bar1 "bar list" | bar2 "bool"
value "bar1 [(bar2 (true))]"
end
end
I'm playing around with these types foo and bar (as a minimal reproducible example) and for some reason, when I try to run "value "foo1 ([(foo2 (2:: nat))] :: foo list)" in a locale, I get a type unification error:
Type unification failed: No type arity foo ::
term_of
Type error in application: incompatible operand type
As you may notice, I tried to explicitly write out the type of each subterm, to no avail
However, "value "bar1 [(bar2 (true))]" returns a value with no error in this locale.
Also more interesting: value "foo1 ([(foo2 (2:: nat))] :: foo list)" works just fine if foo and the value statement are not declared in a locale. I tried looking at StackOverflow pages and searched through threads here to little success. What exactly am I missing? Is this specifically a problem with nats and locales?
Mathias Fleury (Apr 09 2026 at 10:33):don't put datatype declaration in locales
Ant S. (Apr 09 2026 at 10:33):is this a general rule-of-thumb?
Mathias Fleury (Apr 09 2026 at 10:33):the datatype package is not really localized
Mathias Fleury (Apr 09 2026 at 10:34):Sometimes you get errors, sometimes stuff stops working down the line like here
Ant S. (Apr 09 2026 at 10:35):I see
is this in the datatypes manual?
Ant S. (Apr 09 2026 at 10:35):also what do you mean when you say that a package "is not localized"?
Ant S. (Apr 09 2026 at 10:36):what exactly does it mean to localize a package in Isabelle/HOL?
Mathias Fleury (Apr 09 2026 at 10:36):compatible with locales
Ant S. (Apr 09 2026 at 10:36):oh
why is that
Mathias Fleury (Apr 09 2026 at 10:37):from my understanding, there are fundamental issues (see https://isabelle.systems/zulip-archive/stream/336180-Archive-Mirror.3A-Isabelle-Users-Mailing-List/topic/.5Bisabelle.5D.20Datatype.20definition.20in.20locale.20context.html)
Mathias Fleury (Apr 09 2026 at 10:38):so support is only going to be possible for a subset of locales
Ant S. (Apr 09 2026 at 10:38):does this also mean that I can't declare a function over a type in a locale?
Mathias Fleury (Apr 09 2026 at 10:38):So it is not very motivating to fix all the tactics in the BNF package
Ant S. (Apr 09 2026 at 10:38):(or recursive functions in general)
Mathias Fleury (Apr 09 2026 at 10:39):Ant S. said:
does this also mean that I can't declare a function over a type in a locale?
This works as far as I know, but you are going into issues if you want to generate code / use value
Ant S. (Apr 09 2026 at 10:39):oh, I see
Ant S. (Apr 09 2026 at 10:41):Mathias Fleury said:
if you want to generate code / use value
if the function is in the locale?
Ant S. (Apr 09 2026 at 10:41):or if the datatype is (still) in the locale
Ant S. (Apr 09 2026 at 10:46):Is that why you'd get something like "no code equations for fn, requested by dependencies"
Ant S. (Apr 09 2026 at 10:46):where fn is some function
Mathias Fleury (Apr 09 2026 at 11:18):Ant S. said:
Mathias Fleury said:
if you want to generate code / use value
if the function is in the locale?
Yes. There are two issues: code equations depend on the parameters of the locale and second the function are actually abbreviations and the code generator cannot handle that
Mathias Fleury (Apr 09 2026 at 11:19):In practice, this has never really been an issue for me
Mathias Fleury (Apr 09 2026 at 11:19):I never had the case of the termination depending on the local parameters, so moving the function out of the locale was always possible
Last updated: Apr 14 2026 at 09:21 UTC