[isabelle] Isabelle Interval Help
I am just wondering if you know how to create a definition in Isabelle
or Isar over a specific interval.
I am trying to create the Gram-Schmidt Process in Isabelle and have
come across the problem of how to define:
(ith lambda i) = (innerproduct (ith v n) (ith u i))/(innerproduct (ith
u i) (ith u i)) over the interval i = 1,..,(n-1)
I want to calculate each lambda starting with the first lambda and
then finishing on the (n-1)th lambda. Not sure how to do this in
The University of Edinburgh is a charitable body, registered in
Scotland, with registration number SC005336.
[Attachment stripped: Original attachment type: "application/octet-stream", name: "GramSchmidt.thy"]
This archive was generated by a fusion of
Pipermail (Mailman edition) and