Maybe use the choice function to select a pair. I.e., write
@(m,c). .....
?
Michael
On 19 Feb 2020, at 09:30, "jpe...@student.bham.ac.uk"
<jpe...@student.bham.ac.uk> wrote:
Hi
This is a question about using the select operator @ to return multiple values
which depend on each other in HOL Light.
For example when working with polynomial_function defined as
polynomial_function p <=> ?m c. !x. p x = sum(0..m) (\i. c i * x pow i) it
might be useful to be able to use the @ operator to return the upper bound m
and the coefficient function c, however as the choice of m depends on c and
visa versa you cannot use 2 separate select statements. (e.g. if m > degree(p)
then c(n) must be 0 for degree(p)<n<=m )
What is the best way to approach this? Is there a way to return both of the
values or would they have to be "combined together" inside the select statement?
Thanks
James
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
