Re: [isabelle] Vector of bools

On Fri, Mar 25, 2011 at 10:46 AM, Steve W <s.wong.731 at> 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",

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.