Finding elab/syntax functions

Stream: new members

[hakanaras]

What is a good way to find out what functions I need to use to create certain syntax for an elaboration?

For example I want to generate one constructor for each operator in operators, but I can't figure out how to create the syntax and splice it to form the complete inductive type syntax:

private def operators : List (Char × String) :=
  [ ('=', "equals")
  , (':', "colon")
  , (';', "semicolon")
  ]

elab "#genOperatorBasis" : command => do
  let ind <- `(private inductive OperatorBasis2 where)
  Lean.Elab.Command.elabCommand ind

#genOperatorBasis

I've tried running #eval on `(inductive Foo where | foo), but it prints very long expanded code.

[hakanaras]

OK, I figured out how to create the syntax:

  let p <- `(Lean.Parser.Command.ctor| | foo : OperatorBasis2)
  let ind <- `(private inductive OperatorBasis2 where $p)

But I get this error when running the elaborator: Error: invalid 'Name.append', both arguments have macro scopes, consider using 'eraseMacroScopes'. And then the names are not available later on.

[hakanaras]

Lean simply won't make names available if they were constructed within the elaborator monad it seems.

This works, OperatorBasis2 is available afterwards, but OperatorBasis2.foo is not:

syntax (name := genOperatorBasis) "#genOperatorBasis " ident : command

@[command_elab genOperatorBasis]
def mycommand1Impl : CommandElab := fun stx => do
  if let some nameStr := stx[1].isIdOrAtom? then
    let name := mkIdent $ Name.mkSimple nameStr
    let p <- `(Lean.Parser.Command.ctor| | foo : $name)
    let ind <- `(inductive $name where $p)
    Lean.Elab.Command.elabCommand ind
  else
    throwUnsupportedSyntax

#genOperatorBasis OperatorBasis2