@(m,c). .....
?
Michael
On 19 Feb 2020, at 09:30,
"jpe...@student.bham.ac.uk<mailto:jpe...@student.bham.ac.uk>"
mailto: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
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