Michael Soegtrop (Sep 12 2022 at 16:21): Michael Soegtrop (Sep 12 2022 at 16:21):I want to simplify only the arguments of a specific constructor. Maybe one can do this using pattern_occs but I can't figure out the syntax.
E.g. how would I simplify only the argument of the S, but not the right hand side in:
Goal forall a:nat, S (0 + a) = 0 + a.
intros a.
reference_occs btw. only works for function calls, not for constructors.
Paolo Giarrusso (Sep 13 2022 at 05:23):rewrite [S _]/= with ssreflect rewrite should work?
Last updated: Oct 13 2024 at 01:02 UTC