Re: [isabelle] Vector of bools



I see. So if I want to try, say, "real ^ 'n", which libraries do I need to
import? I've tried "HOL/Multivariate_Analysis/Cartesian_Euclidean_Space",
but it takes a very long time to load the import.

Thanks
Steve

On Fri, Mar 25, 2011 at 9:30 PM, Brian Huffman <brianh at cs.pdx.edu> wrote:

> On Fri, Mar 25, 2011 at 10:46 AM, Steve W <s.wong.731 at gmail.com> wrote:
> > I see that one can use real_vector to construct a vector of reals,
>
> First of all, remember that real_vector is a *type class*, not a *type
> constructor*. The real_vector class merely classifies types that
> support scalar multiplication by real numbers.
>
> To actually "construct a vector of reals", you will need to use some
> specific type constructor that is an *instance* of the real_vector
> class. For example, tuples like "real * real" or finite cartesian
> products like "real ^ 'n".
>
> > but is
> > there a way to construct a vector of boolean values, e.g.,
> > <true,false,false...>?
>
> That depends. What kinds of operations on vectors of booleans do you
> require?
>
> You could use the finite cartesian product "bool ^ 'n" from
> Multivariate_Analysis, but that library doesn't provide many
> operations that work with element types besides "real", "complex",
> etc.
>
> Another possibility is to use "bool list". The library provides lots
> of list operations, but unlike type "bool ^ 'n", lists are not
> guaranteed to all have the same length.
>
> A third possibility, if you want vectors of a small constant size, is
> to use ordinary tuples like "bool * bool * bool".
>
> I might be able to help more if you tell me more about what you are
> trying to do.
>
> - Brian
>




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