Shea Levy (Oct 31 2020 at 20:08): Shea Levy (Oct 31 2020 at 20:08):There are straightforward instances of Proper (R ==> R) (λ x, x) and, assuming f and g are proper, Proper (R₁ ==> R₃) (λ x, g (f x)). Do I need to declare these or are the tactics smart enough to find them?
Paolo Giarrusso (Oct 31 2020 at 20:17):no, but
Paolo Giarrusso (Oct 31 2020 at 20:18):if you _name_ g (f x), yes. stdpp’s solve_proper finds those. the stdlib has a solve_proper, but I never tried it.
Paolo Giarrusso (Oct 31 2020 at 20:19):but otherwise, rewrite will search separately for instances for f and g
Last updated: Oct 03 2023 at 02:34 UTC