Re: [isabelle] Vector of bools
Great! That worked. Thanks.
On Mar 29, 2011 4:11pm, Johannes Hölzl <hoelzl at in.tum.de> wrote:
The intended use is to build the HOL-Multivariate_Analysis image:
isabelle make HOL-Multivariate_Analysis
and then select it in ProofGeneral with the Emacs menu:
Isabelle / Logics / Multivariate_Analysis
the building of multivariate analysis takes a couple of minutes but it
is just needed once. Then you just need to import Multivariate_Analysis.
Am Dienstag, den 29.03.2011, 15:37 +0100 schrieb Steve W:
> I see. So if I want to try, say, "real ^ 'n", which libraries do I need
> import? I've
> but it takes a very long time to load the import.
> 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, eg,
> > > ?
> > 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