Re: [isabelle] Vector type syntax



> On 1 Feb 2018, at 12:57, Dominique Unruh <unruh at ut.ee> 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.

The following is not allowed: as the second occurrence of ân is assigned a different sort from the first. This is not how sort assignment normally works, so I think we should see if there is some way to obtain more natural behaviour without forcing hundreds of theorem statements to be altered.

  fixes f :: "real^'n::{finite,wellorder} â real^'n"





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