Stream: Coq users

Topic: Ltac2: Tactic definition must be a syntactical value


view this post on Zulip Janno (Aug 20 2020 at 12:50):

Is there any way to force evaluation of an ltac2 term at definition time of a tactic to get around the Tactic definition must be a syntactical value error? I have a tactic that uses ltac2 to work around ltac1 insufficiencies (taking a list of hint dabases, to be specific) but the workaround is slow (since it parses coq strings into ltac2 idents). This would be fine if I could evaluate the workaround once and stick that into its own tactic but I don't know if there is any way to do that.

view this post on Zulip Janno (Aug 20 2020 at 12:51):

Just to elaborate a bit: eventually all of this needs to be called from ltac1 so a ltac1 tactic notation taking a list of constrs is the best I could come up with


Last updated: Oct 13 2024 at 01:02 UTC