Re: [isabelle] real_vector



real_vector is a type class, i.e. there are different types implementing
a real_vector. For example real, complex, real^'n, (real * real) are all
real vectors.

So "'a :: real_vector set" is a set of type 'a where 'a forms a real
vector space. Hence convex is defined for real, real^'n, real * real,
etc. 

Hope this helps,
  Johannes

Am Dienstag, den 22.03.2011, 16:54 +0000 schrieb Steve W:
> Hi,
> 
> I'm looking at how "real_vector" is used as a type and am somewhat confused
> by examples like:
> 
> definition
>   convex :: "'a::real_vector set \<Rightarrow> bool" ...
> 
> in HOL/Library/Convex.thy. How come "convex" is declared wrt the type
> variable "'a" rather than "real_vector" directly, i.e.
> 
> convex :: "real_vector set..."
> 
> Thank you for any help.
> 
> Steve







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