Generating new inductives from existing

Stream: metaprogramming / tactics

[Tomás Díaz]

I was wondering if it is possible to do something like this, from MetaCoq, where you generate a new inductive using metaprogramming. In this example, it creates a new inductive, e.g. bool' , and adds a new constructor, but one can imagine other use cases.
I know some is possible just using macros, but I haven't found other similar examples as the one I mentioned before.

[Jireh Loreaux]

It's certainly possible, but I don't think macros are the way you want to go. What all do you know about metaprogramming in Lean? Have you read the metaprogramming book? It doesn't cover all the things you would need (e.g., here you're going to need to be adding things to the environment).

[Tomás Díaz]

No, definitely don't want to use macros. I've read the book but I guess I'm a bit at a loss with how to extend the environment with the new definitions (type, constructor, etc.). I'm comparing it now to metacoq's tmMkInductive that adds an inductive, although the term there includes a constructor for inductives.

[Jannis Limperg]

docs#Lean.addDecl is the function that adds declarations to the environment. You can call this with a docs#Lean.Declaration object representing an inductive type to be added.

[Tomás Díaz]

interesting! thanks