Re: [isabelle] Vector type syntax



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


	Makarius




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