Working with TSyntax and cdot

Stream: lean4

[Jon Eugster]

I'm trying my hands on writing tactics and I could need some help. I can manually create single tactic calls (type TSyntax `tactic) like cmd below, but how would I combine these syntax elements into a structured tactic instruction using · (i.e. when there are multiple goals)?

For context, my goal is to create a logInfo message that tells accurately what e.g. ext did, which also includes focusing on newly created subgoals.

import Std

open Lean Meta Elab Tactic Term

variable (lemma₁ lemma₂ lemma₃ : Name)

def createTacticBlock (goal : MVarId) : MetaM (PUnit) := goal.withContext do
    let mut myTactics : Array (TSyntax `tactic) := #[]

    -- create some tactic calls
    let cmd ←`(tactic| apply $(mkIdent lemma₁))

    myTactics := myTactics.push cmd

    -- Now instead of creating a list, create some valid tactic syntax that applies to multiple
    -- goals, like:
    --
    -- · apply lemma₁
    --   apply lemma₂
    -- · apply lemma₃

    logInfo m!"{myTactics}"

[Jon Eugster]

( I should say I'm mainly hacking at this point and have quite a hard time understanding the Metaprogramming book. I barely know anything about the different monads and only scrap together things from what I see in the source code, I might be going at this the wrong way :sweat_smile: )

[Mario Carneiro]

· is a tactic, specifically of the form · $tac:tacticSeq

[Mario Carneiro]

so you can create one the same as any other tactic, you just use `(tactic| · foo; bar) or whatever

[Mario Carneiro]

It's not really clear to me what exactly you want to put in that function though, there are a lot of placeholders

[Mario Carneiro]

I think you probably want createTacticBlock to have a type like MetaM Syntax.Tactic or MetaM (Array Syntax.Tactic) so that it can call itself recursively

[Jon Eugster]

Mario Carneiro said:

· is a tactic, specifically of the form · $tac:tacticSeq

oh. that's a tad simpler than expected.

[Jon Eugster]

I agree createTacticBlock has the wrong type in the MWE, I just copied that from applyExtLemma.

I was going to construct a Syntax.Tactic term or someting in a IO.Ref and then just add to that in the relevant funtion calls. Something like

initialize usedExtLemmas : IO.Ref (Array (TSyntax `tactic)) ← IO.mkRef #[]