A higher-level interface to `addDecl`?

Stream: general

[Sabrina Jewson]

I’m writing a command elaborator that generates declarations. Is there any higher-level interfact I can use that wraps addDecl internally? Specifically, to repeated frustration I’ve already encountered the following few things feel like they could be done automatically, but I’m not sure how:

1. Prefixing the name of the resulting declaration with the currently opened namespace;
2. Dealing with variables, automatically converting them to parameters iff they’re used;
3. Conversion of universe level params / metavariables into level parameters of the declaration;
4. Marking the declarations with abbrev;
5. Elaborating the value of the definition with appropriate usage of withDeclName.

I don’t even know how to achieve (1) and (4) right now, so help with that would also be appreciated. Alternatively, if there is a complete example out there of something similar to this, it would be very helpful.

[Mario Carneiro]

you can always adapt the body of src#Lean.Elab.Command.elabDeclaration . There is a lot though (main code is in src#Lean.Elab.Term.elabMutualDef.go and src#Lean.Elab.addPreDefinitions ), it would be great to have a metaprogramming interface to get the bells and whistles

[Sabrina Jewson]

Ah, thank you! I searched around a lot for elabDef, elabAbbrev but didn’t find that one :sweat_smile:

[Mario Carneiro]

regarding questions (1) and (4):

• the way the def syntax resolves the declaration name from the parsed name is src#Lean.Elab.mkDeclName
• the only thing that abbrev seems to do is set ReducibilityHints.abbrev in the defnDecl passed to the kernel (which is surprising, in particular it is not marked as reducible AFAICT)

[Scott Morrison]

If you would like to contribute a metaprogramming interface that gives access to the functionality of elabDeclaration, Std or Mathlib would love to have it.

We would like to provide more MetaM and TacticM level interfaces in Lean itself... Eventually!

[Kyle Miller]

@Mario Carneiro You scared me with your second bullet point, and I got a chance to try to read through the source. For abbrev, the reducible and inline attributes are added here as it constructs the DefView.

[Mario Carneiro]

oh sneaky, it's a syntax fixup

[Mario Carneiro]

I was looking for calls to setReducibleAttribute or uses of .abbrev