Email Gateway (Aug 18 2022 at 13:43): Email Gateway (Aug 18 2022 at 13:43):From: Peter Lammich <peter.lammich@uni-muenster.de>
Hi all,
the reference manual says:
"The configuration option depth limit limits the number of recursive
invocations
of the simplifier during conditional rewriting."
However, there seems to be no documentation how to set this
configuration option (?).
How to set the depth-limit? Best would be locally just for one
invokation of the simplifier, something like
apply (simp depth_limit=4) [This does not work]
Regards,
Peter
Email Gateway (Aug 18 2022 at 13:43):From: Tobias Nipkow <nipkow@in.tum.de>
You currently have to do it via the Proof General settings menu.
Tobias
Peter Lammich schrieb:
Email Gateway (Aug 18 2022 at 13:44):From: Tobias Nipkow <nipkow@in.tum.de>
Sorry, I was thinking of the Trace Simp Depth limit. What you want is
declare [[simp_depth_limit = 6]]
Tobias
Peter Lammich schrieb:
Last updated: May 03 2024 at 08:18 UTC