Email Gateway (Aug 22 2022 at 11:20): Email Gateway (Aug 22 2022 at 11:20):From: Andreas Lochbihler <andreas.lochbihler@inf.ethz.ch>
Dear Eisbach experts,
I would like to use the tactic method inside a method definition with Eisbach.
Here is a minimal example:
method foo = (tactic {* Transfer.transfer_step_tac @{context} 1 *})
Obviously, this does not work, because the proof tactic requires a context and using
@{context} gives the compile-time context, while I should rather use the context at the
invocation site. Is there a way to access the dynamic context from within an Eisbach
method definition? Or do I have to wrap the tactic expression in a method definition first?
Best,
Andreas
Email Gateway (Aug 22 2022 at 11:21):From: Daniel Matichuk <daniel.matichuk@nicta.com.au>
Currently there is no standard way to directly access the run-time context inside of an Eisbach method. In general the use of the "tactic" method in Eisbach is not well supported, mostly
due to not handling ML antiquotations as one might expect. The usual approach here is indeed to first lift your underlying tactic into a method with method_setup.
The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.
Last updated: Nov 21 2024 at 12:39 UTC