passing list into a tactic

Stream: general

[Frederick Pu]

I'm trying to figure out how pass a list into a tactic that uses [,*] But I can't figure out how to get it to work:

elab "mysimp " "[" l:ident,* "]" : tactic => do
  let idents := l.getElems
  let names := idents.map (fun idSyntax => idSyntax.getId)
  Elab.Tactic.evalTactic <| ← `(tactic| simp (config := {singlePass := true}) only [$(names.map mkIdent),*])

[Edward van de Meent]

here's a fix:

import Lean
open Lean Elab Macro Tactic

elab "mysimp " "[" l:ident,* "]" : tactic => do
  let idents := l.getElems
  let names := idents.map (fun idSyntax => idSyntax.getId)
  let idents' := names.map mkIdent
  Elab.Tactic.evalTactic <| ← `(tactic| simp (config := {singlePass := true}) only [$(⟨names.map (mkIdent ·)⟩),*])

[Edward van de Meent]

i added anonymous constructor notation as well as the dot lambda notation to make all the coercions be inserted at the right place

[Aaron Liu]

Is there a reference for these things?

[Edward van de Meent]

not that i know of. i found this mostly by looking through the #docs, searching for what makes the type error happen

[Edward van de Meent]

i.e. looking up why Array and Lean.Syntax.TSepArray aren't the same

[Edward van de Meent]

you can find some info about antiquotations in the metaprogramming book under the "macro" section, but it's not comprehensive... there might in the future be something more explicit in the language reference though

[Aaron Liu]

New error acquired

import Lean

open Lean

elab "mysimp " "[" l:ident,* "]" : tactic => do
  let idents := l.getElems
  let names := idents.map (fun idSyntax => idSyntax.getId)
  Elab.Tactic.evalTactic <| ← `(tactic| simp (config := {singlePass := true}) only [$[$(names.map mkIdent)],*])

[Frederick Pu]

thx!

[Frederick Pu]

so does the anomous constructor lift Syntax?

[Kyle Miller]

import Lean

open Lean

elab "mysimp " "[" idents:ident,* "]" : tactic => do
  Elab.Tactic.evalTactic <| ← `(tactic| simp (config := {singlePass := true}) only [$[$idents:ident],*])

[Kyle Miller]

By the way, you can write simp +singlePass instead of simp (config := {singlePass := true}) now.

[Kyle Miller]

anonymous constructor notation

I think anonymous constructor notation should be avoided in syntax quotations. There are some uses for it (some functions return Syntax instead of something more specific), but it's a good way to create malformed syntax.

It should especially be avoided if it's done without any syntax kind annotations, since then you have no idea what it's being interpreted as.

[Edward van de Meent]

that's a fair point