Stream: math-comp users

Topic: how to do remember ... as

view this post on Zulip walker (Nov 05 2022 at 10:23):

What is the mathcomp idiomatic way of doing remembr (f x) as y ?
The reason is that I want to do induction over y.

view this post on Zulip Ana de Almeida Borges (Nov 05 2022 at 11:57):

move eqfxy: (f x) => y.

Last updated: Feb 08 2023 at 04:04 UTC