Re: [isabelle] Specializing types in locales

On Fri, Oct 29, 2010 at 10:32 AM, Mathieu Giorgino
<mathieu.giorgino at> wrote:
> locale foo3_loc =
>  fixes bar :: "'a"
>  fixes foo :: "'a"
> begin
> definition "foobar = (foo, bar)"
> end
> (*
> locale foo3_nat_loc = foo3_loc +
>  constrains bar :: "nat"
>  constrains foo :: "nat"
> Error: Failed to meet type constrain
> *)

Note that when you have separate "constrains" clauses, they are
applied one at a time. You can't constrain the type of "bar" by
itself, because then it doesn't have the same type as "foo", which the
function "foobar" requires.

However, it works if you declare both type constraints simultaneously.
(I tested this with Isabelle2009-2.)

locale foo3_nat_loc = foo3_loc +
  constrains bar :: "nat" and foo :: "nat"

The same trick also works on all the other examples in your file that
I tried it on.

Hope this helps,
- Brian

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.