Folding Syntax

Stream: metaprogramming / tactics

[Francisco Lima]

I am making a custom tactic and in it it will suggest the steps it took, so it needs to both keep track of individual steps and a general route.

So for now my tactic uses a helper function that return a list o TSyntax [`tactic] (needs to be this for the addSuggestion later) but when folding said list I come upon a problem where once I append 2 nodes using `(tactic| $(acc); $(e)) it gives a TSyntax[`tactic.seq] making the very expression for the folder not work, how can I circumvent that? be it a better folding expression or another way to keep track of the tactics used.

[Aaron Liu]

Why not just suggest a tacticseq?

[Aaron Liu]

If you really need a tactic then wrapping a tacticseq in parentheses gives back a tactic

[Francisco Lima]

solved using raw String and constructing the suggestion by hand, but now I am having problems with Qq Matching