Email Gateway (Oct 28 2020 at 09:55): Email Gateway (Oct 28 2020 at 09:55):From: Lawrence Paulson <lp15@cam.ac.uk>
Is there a less ugly to express this?
qed (use in ‹fastforce+›)
Omitting the “use in” yields an error message: Undefined method: "cartouche"
Larry
Email Gateway (Oct 28 2020 at 10:05):From: Jakub Kądziołka <kuba@kadziolka.net>
I might be missing something, but the following syntax, without any
cartouche, seems to work for me:
qed fastforce+
Regards,
Jakub Kądziołka
Email Gateway (Oct 28 2020 at 10:52):From: Lawrence Paulson <lp15@cam.ac.uk>
I guess I simplified it too much. But is there something similar for
qed (force simp: add_ac+)
?
Larry
Email Gateway (Oct 28 2020 at 10:54):From: Manuel Eberl <eberlm@in.tum.de>
What about
qed (force simp: add_ac)+
Manuel
Last updated: Jan 04 2025 at 20:18 UTC