Jonas Stahl (Aug 09 2024 at 11:55): Jonas Stahl (Aug 09 2024 at 11:55):Hi everyone,
I am using the Interface for adding functions: "Function.add_function", which is applied onto my current local_theory lthy and yields a new local_theory lthy'.
In order to prove the termination I have a custom tactic, that needs to prove this lemma first: "name_dom a".
Sadly the function "Syntax.read_prop" is not able to parse the lemma using the local_theory lthy' yielded by "Function.add_function".
I can achieve the intended behaviour by closing the local_theory to a theory and opening a local_theory again afterwards with the following code: Named_Target.theory_init (Local_Theory.exit_global lthy)
I there a better way to achieve the intended behaviour?
Kevin Kappelmann (Aug 09 2024 at 12:38):add_function also returns the Function_Common.info, which contains the record field #dom - I think that's what you are looking for.
Jan van Brügge (Aug 09 2024 at 13:35):If your tactic works by using a well-founded relation, this example might also help: https://github.com/jvanbruegge/binder_datatypes/blob/master/Tools/mrbnf_recursor.ML#L770
https://github.com/jvanbruegge/binder_datatypes/blob/master/Tools/mrbnf_recursor_tactics.ML#L44
Jonas Stahl (Aug 09 2024 at 15:24):Kevin Kappelmann said:
add_functionalso returns theFunction_Common.info, which contains the record field#dom- I think that's what you are looking for.
This worked for me. Thanks to both of you :)
Last updated: Dec 21 2024 at 16:20 UTC