Adding an instance programmatically

Stream: lean4

[Andrej Bauer]

How would I go about adding a new instance programmatically, in the style of addDecl? I've searched around a bit but can't find anything.

[Alex Keizer]

Well, a class instance is nothing more than a normal definition with the instance attribute. The instance notation is just syntactic sugar for @[instance] def. (You should double check the name of the modifier, it might be inst or some variation instead).

[Alex Keizer]

So, to add an instance programatically is to add a definition, with this attribute, programatically

[Yaël Dillies]

Note you might also want to tag it protected (this was the Lean 3 behavior).

[Andrej Bauer]

So not Lean.Meta.addInstance?

[Andrej Bauer]

So which function concretely would one use? It looks like addDecl doesn't allow me to provide any attributes.

[Moritz Doll]

it should be docs4#Lean.Meta.addInstance

[Moritz Doll]

https://github.com/leanprover/lean4/blob/f9da1d8b55ca6989297fb952985b7d8d6c77e14b/src/Lean/Meta/Instances.lean#L190-L195
below the code you see what the attribute does: it basically just calls addInstance after figuring out the priority

[Andrej Bauer]

Thanks. I am trying to do this in Elab.Command.CommandElabM but Meta.addInstance is in MetaM monad. How to get from one to the other?

[Andrej Bauer]

Woohoo, it's Lean.Elab.Command.liftTermElabM. This would be no fun with documentation :-)

[Siddharth Bhat]

I am surprised that we need to manually invoke Lean.Elab.Command.liftTermElabM. Ought these not automatically lift with do notation?

[Alex Keizer]

Maybe there is no automatic lifting so that people have to make a (more) concious choice between liftTermElabM and runTermElabM?

[Kyle Miller]

In case it helps, I had to figure out some of these things to make some derive handlers (for Fintype, for ToExpr).

In the Fintype derive handler, I added instances by creating a Syntax object and using elabCommand (see mkFintype).

The ToExpr derive handler uses various helper functions that are useful for adding additional arguments (like, in this case, adding ToExpr instance arguments when your type has parameters). These functions are not very documented, and I had to read the source...

You can also look at Lean 4 core's deriving handlers for more examples of creating instances.

[Kyle Miller]

Re liftTermElabM, my understanding is that there is additional state in the TermElabM (like the metavariable context and the list of pending synthetic metavariables), so it makes sense that you need to explicitly lift.