write a tactic that accepts at most 5 tactics

Stream: general

[Zihao Zhang]

How can I write a tactic that accepts at most 5 tactic arguments and doesn't consume tactics outside the current scope? In the following example, it should not match · simp

import Mathlib
open Lean Elab IO Meta Tactic in
elab "my_tool" tac:tactic ";"?
  tac2:optional(tactic) ";"?
  tac3:optional(tactic) ";"?
  tac4:optional(tactic) ";"?
  tac5:optional(tactic) :tactic => do
    evalTactic tac
    if let some stx2 := tac2 then evalTactic stx2
    if let some stx3 := tac3 then evalTactic stx3
    if let some stx4 := tac4 then evalTactic stx4
    if let some stx5 := tac5 then evalTactic stx5

example {a b : ℝ} (h1:a+1=1+1): (a + b)^2 = a^2 + 2 * a * b + b^2∧ true := by
  constructor
  · rw [pow_two]
    my_tool
    skip
    skip
    skip
    ring
  · simp

[Aaron Liu]

For not accepting the tactics "out of scope", you probably want some indentation restrictions.

[Jon Eugster]

I'd probably consider using a docs#Lean.Parser.Tactic.tacticSeqIndentGt and then manually write some logic to check for the number of tactics and the "allowed" tactics in that sequence