Re: [isabelle] Specializing types in locales



Thanks Brian and Clemens,

The Brian's solution worked well but it was still necessary to contrains all 
parameters.

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-
July/msg00111.html
> > 
> > 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-
July/msg00033.html
> > Is this still a possibility?

Thanks,

Mathieu




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