Re: [isabelle] Vector type syntax



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.

Best wishes,
Dominique.




On 1 February 2018 at 14:28, Lawrence Paulson <lp15 at cam.ac.uk> wrote:

> Vector types, similar to those in HOL Light, have been available for some
> time: real^ân abbreviates (real, 'n) vec, where ân is some finite index
> type. But a number of theorems require an ordering on that type, so we
> sometimes see types such as (real, 'n::{finite,wellorder}) vec. Such types
> cannot be written as real^ân because that syntax constrains the sort on ân
> to {finite}.
>
> What can we do about this? Is it possible to separate the âa^ân syntax
> from any specific sort constraints on the type ân? And if not, should it
> use the sort constraint {finite,wellorder} instead? Every finite type can
> be well ordered, even without the axiom of choice, so the sort constraint
> {finite} is not really more general than {finite,wellorder}.
>
> Larry Paulson
>
>
>
>
>



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