Re: [isabelle] 'where'-clause for defining locales

Am 30.06.2014 21:27, schrieb Andreas Lochbihler:
> Hi René,
> there is the context element "constrains" that can achieve this to some
> extend. This works best if you constrain the types of all parameters of
> the imported locale that are affected. 

Unfortunately, all parameters are affected, so there is no gain here.
But the 'constrains' provided the idea for the 'constraining'-thing in
my email.

(Also: 'constrains' is marked as deprecated, so I'd better avoid it in
new developments)

>> P.S.: The same problem arises, when the only parameter using all
>> relevant type variables is the very last one of the imported locale.
> In that case, there is a simple trick using the wildcard _ in the import
> expression. These wildcards are treated like parameters not mentioned
> and are therefore added implicitly to the head of the for clause, as you
> desire.
> locale l3 = fixes p1 :: 'a and p2 :: 'b and p3 :: "'a + 'b"
> locale l4 = l3 _ _ p3
>   for p3 :: "'b + 'b"
>   +
>   fixes p4 :: 'b

Ah, forgot about those.

Thanks a lot,

René Neumann

Institut für Informatik (I7)
Technische Universität München
Boltzmannstr. 3
85748 Garching b. München

Tel: +49-89-289-17232
Office: MI 03.11.055

Attachment: smime.p7s
Description: S/MIME Cryptographic Signature

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