Re: [isabelle] real_vector



On Wed, 23 Mar 2011 07:19:54 Johannes Hölzl wrote:
> 1) The types in the type class real_vector only contain vectors
> of reals. So it is not necessary to specify this explicitly.
> 
>    it is enough to say:
> 
>    consts v :: "'a real_vector"

Do you mean this?

consts v :: "'a::real_vector"

Tim
<><

Attachment: signature.asc
Description: This is a digitally signed message part.



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