lean 4 macro + loop

Stream: mathlib4

[Yury G. Kudryashov]

I want to try to autogenerate parts of the FTC file. My idea is to have a macro that outputs one of many similar theorems, then call it in a nested loop with different settings. Where can I read about the syntax?

[Yury G. Kudryashov]

Probably, I can write a template in something like jinja2 or mako templates but this is not the Lean way.

[Mario Carneiro]

The nearest example of such a thing is Mathlib.Data.UInt

[Yury G. Kudryashov]

Thank you!

[Yury G. Kudryashov]

I'm trying to do it in a simpler case and I don't know how to make lemma names from string concatenation of arguments and fixed parts.

[Yury G. Kudryashov]

import Mathlib.Algebra.Opposites

/-- If `M` multiplicatively acts on `α`, then `DomMulAct M` acts on `α → β` as well as some
bundled maps from `α`. This is a type synonym for `MulOpposite M`, so this corresponds to a right
action of `M`. -/
@[to_additive "If `M` additively acts on `α`, then `DomAddAct M` acts on `α → β` as
well as some bundled maps from `α`. This is a type synonym for `AddOpposite M`, so this corresponds
to a right action of `M`."]
def DomMulAct (M : Type _) := MulOpposite M

@[inherit_doc] postfix:max "ᵈᵐᵃ" => DomMulAct
@[inherit_doc] postfix:max "ᵈᵃᵃ" => DomAddAct

namespace DomMulAct

/-- Equivalence between `M` and `Mᵈᵐᵃ`. -/
@[to_additive "Equivalence between `M` and `Mᵈᵐᵃ`."]
def mk : M ≃ Mᵈᵐᵃ := MulOpposite.opEquiv

/-!
### Copy instances from `Mᵐᵒᵖ`
-/

set_option hygiene false in
run_cmd
  for n in [`Mul, `One, `Inv, `Semigroup, `CommSemigroup, `LeftCancelSemigroup,
    `RightCancelSemigroup, `MulOneClass, `Monoid, `CommMonoid, `LeftCancelMonoid,
    `RightCancelMonoid, `CancelMonoid, `CancelCommMonoid, `InvolutiveInv, `DivInvMonoid,
    `InvOneClass, `DivInvOneMonoid, `DivisionMonoid, `DivisionCommMonoid, `Group,
    `CommGroup] do
  let idnt := Lean.mkIdent n
  let instName := "inst" ++ n
  Lean.Elab.Command.elabCommand (← `(
    @[to_additive] instance $instName [$idnt Mᵐᵒᵖ] : $idnt Mᵈᵐᵃ := ‹_›
  ))

[Yury G. Kudryashov]

Without let instName := ... and $instName after instance, it works.