Email Gateway (Aug 17 2022 at 14:44): Email Gateway (Aug 17 2022 at 14:44):From: Peter <views@gmx.de>
I have two locales:
locale A =
fixes f :: "'a => 'b"
locale B =
fixes g :: "'b => bool"
Now I want to combine these two, so that the types 'b in A and B are the
same.
The approach:
locale C = A + B
lemma (in C) "g (f a)"
gives a type error when trying to type the lemma.
I'm currently using the dirty-hack:
locale C = A + B +
assumes "False => g (f a)"
lemma (in C) "g (f a)"
this works but looks not clean.
Is there any cleaner way to do that ?
Thanks for any help in advance
Peter
Email Gateway (Aug 17 2022 at 14:44):From: Clemens Ballarin <ballarin@in.tum.de>
Peter wrote:
Type constraints on parameters may be added with the context element
constrains:
locale C = A + B +
constrains f :: "'a => 'b"
and g :: "'b => bool"
does what you want.
Clemens
Email Gateway (Aug 17 2022 at 14:44):From: Peter <views@gmx.de>
Clemens Ballarin wrote:
Thank you, that helped.
Perhaps one should add, that one should constrain all parameters. I now
have something like:
locale A =
fixes
f :: "'a set => 'l => 'l" and
x :: "'l"
locale B = A +
constrains
f :: "'a set => 'l => 'l" and
x :: "'l"
fixes g :: "'a set list => 'l => 'l"
This works, but if I drop the type constraint on x, I get the error:
*** exception TYPE raised: unify_parms: failed to unify types ?'b and 'b
*** At command "locale".
But the typing of x should be clear from the declaration in A and the
constraint on f (isn't it ?).
Peter
Email Gateway (Aug 17 2022 at 14:46):From: Clemens Ballarin <ballarin@in.tum.de>
Peter wrote:
Thanks for pointing this out. This is probably a bug.
Clemens
Last updated: May 03 2024 at 12:27 UTC