Re: [isabelle] Specializing types in locales
- To: cl-isabelle-users at lists.cam.ac.uk
- Subject: Re: [isabelle] Specializing types in locales
- From: Mathieu Giorgino <mathieu.giorgino at irit.fr>
- Date: Tue, 2 Nov 2010 12:02:39 +0100
- In-reply-to: <email@example.com>
- Organization: IRIT
- References: <firstname.lastname@example.org> <email@example.com>
- User-agent: KMail/1.13.5 (Linux/2.6.35-ARCH; KDE/4.5.2; x86_64; ; )
Thanks Brian and Clemens,
The Brian's solution worked well but it was still necessary to contrains all
With Clemens' one, it is not any more necessary: the type is constrained once
for all parameters.
However, is there anyone having a clue about my last question?
> > A great feature would be to have specializable
> > type declarations but I've understood it wasn't possible due to the
> > logical framework (quantification on types) in an email from Makarius:
> > https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2009-
> > I know I could also use AWE, but there is no release for Isabelle 2009-2
> > (but I haven't tried the one for Isabelle 2009-2 that could perhaps also
> > work).
> > Furthermore in an other mail, Makarius said:
> > Trying a bit harder in the internal structures, one could support type
> > parameters on the RHS one day.
> > https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2010-
> > Is this still a possibility?
This archive was generated by a fusion of
Pipermail (Mailman edition) and