Re: [isabelle] Vector type syntax



Am Freitag, den 02.02.2018, 21:45 +0100 schrieb Makarius:
> On 01/02/18 13:57, Dominique Unruh wrote:
> > The constraints imposed by ^ are relatively half-hearted in any case. The
> > following types are accepted:
> > 
> > typ "real^real"
> > type_synonym 'a id = "'a"
> > typ "real^('n::{finite,wellorder} id)"
> > typ "real^('n::{wellorder} id)"
> > 
> > The reason is that the parse translation adds the ::{finite} constraint
> > only if the second argument to ^ is a type variable.
> > 
> > It feels to me that no enforcement might be better than such half-hearted
> > enforcement.
> 
> Yes, probably.
> 
> Note that this hard-wired policy comes from the following changeset by
> Johannes HÃlzl:
> 
> changeset:   34290:1edf0f223c6e
> user:        hoelzl
> date:        Thu Jan 07 17:43:35 2010 +0100
> files:       src/HOL/Multivariate_Analysis/Finite_Cartesian_Product.thy
> description:
> added syntax translation to automatically add finite typeclass to index
> type of cartesian product type
> 

As fas as I remember this changeset is from a time when we didn't have a euclidean_space type class.
Since then most occurrences of "'a ^ 'n" are replaced by "'a :: euclidean_space" in HOL-Analysis.
I'm okay if somebody wants to change this again.

Also I'm not sure what's the situation in the AFP (espeially Joses entries) and IsarFoR which uses
some finite dimensional modules (i.e. 'a::ring ^ 'n) .

 - Johannes









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