Email Gateway (Aug 22 2022 at 09:21): Email Gateway (Aug 22 2022 at 09:21):From: Manuel Eberl <eberlm@in.tum.de>
Hallo,
I noticed that setsum.cong, setprod.cong etc. are not declared as
fundef_cong. This is important for function-package function definitions
where a recursive call occurs under a setsum or setprod. Without these
declarations.
Is there a reason not to put these declarations into Groups_Big? If not,
is it unproblematic to simply add the declaration to the cong lemma in
the locale comm_monoid_set, or should only setsum.cong and setprod.cong
be declared as fundef_cong rules explicitly?
Cheers,
Manuel
Last updated: Apr 19 2024 at 20:15 UTC