Email Gateway (Oct 20 2026 at 22:01): Email Gateway (Oct 20 2026 at 22:01):From: Mete Polat <mete@varto.com>
Subject: [isabelle] Does record syntax intentionally ignore aliases of hidden constructor names?
Hi everyone,
Is record-literal syntax intentionally independent of constructor name-space aliases? I observe the following in Isabelle2025-2 and Isabelle2026-RC4:
theory Record_Constructor_Repro
imports Main
begin
record public_record = public_field :: nat
record hidden_record = hidden_field :: nat
ML ‹
val hidden_constructor = @{const_name hidden_record.hidden_record_ext};
val public_constructor = @{const_name public_record.public_record_ext};
›
value "hidden_record.hidden_record_ext 1 () = ⦇hidden_field = 1⦈"
text ‹Hide the second record's constructor, then give its name to the
first record's constructor as an alias.›
hide_const hidden_record.hidden_record_ext
setup ‹Sign.const_alias (Binding.qualified_name hidden_constructor) public_constructor›
text ‹The name now resolves to the public constructor›
value "(hidden_record.hidden_record_ext 1 () :: public_record)"
text ‹But record syntax still constructs a hidden_record using the original
hidden constructor, despite that constructor name now resolving elsewhere.›
value "(⦇hidden_field = 1⦈ :: hidden_record)"
text ‹Clash of types "_ public_record_scheme” and "_ hidden_record_scheme"›
value "hidden_record.hidden_record_ext 1 () = ⦇hidden_field = 1⦈"
end
In the final value, the record literal remains valid and uses the original hidden constructor after that constructor’s name has been hidden and aliased to a different constructor. Is this intended?
Best,
Mete
Email Gateway (Oct 25 2026 at 08:05):From: Lars Hupel <lars@hupel.info>
Subject: [isabelle] Does record syntax intentionally ignore aliases of hidden constructor names?
Hi Mete,
Is record-literal syntax intentionally independent of constructor name-space aliases?
I believe that the record syntax is older than local theories and
namespaces in Isabelle.
You may want to try instead HOL-Library.Datatype_Records, which provides
the same syntax but uses BNF's more modern machinery under the hood. (I
have never tested it under the presence of namespace modifications,
though.) The downside of that package is that extensible records are not
supported, since I never had a use for them.
Cheers
Lars
Last updated: Oct 29 2026 at 04:52 UTC