command loop

Stream: lean4

[Alexander Bentkamp]

Is it possible to write a command that runs other commands in a for loop? Something like this:

for i in [:10] do
    `(#check $i)

This would print the numbers from 0 to 9 in the infoview.

Or:

for i in [:10] do
    `(def $(`number ++ Name.mkNum $i) := $i)

which would add definitions of constants number0 to number9 to the environment.

I don't really know how useful it would be, but I think it's a fun idea.

[Mario Carneiro]

I would just think of that as runCmd

[Mario Carneiro]

import Mathlib.Tactic.RunCmd

open Lean Elab Command
run_cmd
  for i in [:10] do
    elabCommand $ ← `(#check $(Quote.quote i))

[Alexander Bentkamp]

Oh wow, I didn't know about run_cmd! Thanks!