[isabelle] Define a list over an interval
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> "
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.
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