Email Gateway (Aug 18 2022 at 11:32): Email Gateway (Aug 18 2022 at 11:32):From: RF Todd <R.F.Todd@sms.ed.ac.uk>
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
Last updated: May 03 2024 at 12:27 UTC