Appending tactic sequences

Stream: lean4

[Siddhartha Gadgil]

Is there a good way to append a tactic sequence to another (and to a byTacticSeq)? My present hack is:

(← `(tacticSeq|
            $tacticCode
            ($script)))

which means the second one is in parenthesis.

[Mario Carneiro]

yep that's the standard approach

[Siddhartha Gadgil]

Related question: is there a delaborator for a tacticSeq?

[Mario Carneiro]

what would that mean?

[Mario Carneiro]

tacticSeq only exists as syntax

[Siddhartha Gadgil]

I mean to go from Syntax to Format

[Mario Carneiro]

that's a 'formatter' in lean parlance

[Mario Carneiro]

and yes, you can format any syntax category

[Mario Carneiro]

docs4#Lean.PrettyPrinter.formatCategory