Re: [Hol-info] Using @ for multiple selections in HOL Light

2020-02-20 Thread jpe...@student.bham.ac.uk
@(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

[Hol-info] Using @ for multiple selections in HOL Light

2020-02-18 Thread jpe...@student.bham.ac.uk
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