# [isabelle] Define a list over an interval

Hi,

`Just wondering if any of you know how to define an list over an
``interval? I want to use it within the following definition:
`
consts lambda_term :: "vector \<Rightarrow> vector \<Rightarrow> "
defs
lambda_term_def: "lambda_term (ith \<lambda> i) == (innerproduct (ith
v n) (ith u i))/(innerproduct (ith u i) (ith u i))"
Where u,v are vectors and Lambda is a scalar. I am trying to run it
over the interval where n is a fixed variable which can be any number,
and i runs from 1 to (n-1). I wonder if you are about at all today?

`i.e. I might use v_4 which would find the answer for lambda_1,
``lambda_2, and lambda_3.
`
Rachel
--
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.

[Attachment stripped: Original attachment type: "text/plain", name: "unnamed"]

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