Re: [isabelle] real_vector



2011/3/22 Johannes Hölzl <hoelzl at in.tum.de>

> 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.
>

I see. So if I'd like, say, a const v to be a real vector of reals, how do I
go about that? 'consts v :: "real real_vector"' doesn't seem to be right.

Thanks
Steve


> 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.