Email Gateway (Aug 18 2022 at 13:55): Email Gateway (Aug 18 2022 at 13:55):From: Peter Lammich <peter.lammich@uni-muenster.de>
Hi all.
I have a problem with a definition in a locale context, that causes
strange errors when declaring other locales depending on that locale.
The following example works well if the definition is done after the
declaration of the locale B.
However, if the definition is done before the declaration of B, I get
the following error when trying to declare B:
*** Type unification failed
*** Cannot meet type constraint:
*** Term: empty :: 'a
*** Type: 's
*** At command "locale".
Even more surprisingly, I get the same error when using "abbreviation"
instead of "definition".
What is going on here? How to declare locale B correctly?
Regards & thanks in advance for any hints,
Peter
locale A =
fixes a :: "'s => 'x set"
fixes emp :: "'s"
fixes ins :: "'x => 's => 's"
assumes
"a (ins x s) = insert x (a s)"
"a emp = {}"
-- "This def. causes the next locale command to fail. If removed,
everything will work."
definition (in A) "sng x == ins x emp"
locale B = A +
constrains a :: "'s => 'x set"
fixes m :: "'x => 's => bool"
assumes "m x s = (x : a s)"
-- "If done here, everything is o.k."
definition (in A) "sng x == ins x emp"
Email Gateway (Aug 18 2022 at 13:55):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi Peter,
it works if you explicitly constrain all fixes:
locale B = A +
constrains a :: "'s => 'x set"
and emp :: "'s"
and ins :: "'x => 's => 's"
fixes m :: "'x => 's => bool"
assumes "m x s = (x : a s)"
I do not know the exact reason for this, but I suppose it has something
to do with the way constrain elements are handled by type inference.
Florian
signature.asc
Last updated: May 03 2024 at 12:27 UTC