Extract type and value from name for proof

Stream: lean4

[Thomas Murrills]

If I want to read off the type and proof from a theorem, I can do that using getConstInfo, then extract the .type and value?. Is this the best way to do it when constructing a proof on the meta level? My intuition is that axioms should also be usable to construct a proof, but they don't seem to have a value.

[Eric Wieser]

You shouldn't be using the proof of the theorem, you should refer to it by name

[Thomas Murrills]

Ah, via .const?

[Kyle Miller]

Yeah, but it seems like it's usually written as mkConst (like in mkConst ``propext []). There are a number of helper functions for it to fill in universe metavariables too.

[Kyle Miller]

like mkConstWithFreshMVarLevels

[Kyle Miller]

There's also mkAppM, which makes sure everything fully typechecks (and fills in implicit arguments, well most of them, see the docstring) when you give it some arguments, like mkAppM ``Subsingleton.elim #[lhs, rhs]

[Thomas Murrills]

Ah, I see, thanks! (I saw that I had a ConstantInfo and immediately forgot all about .const and friends, asking myself “how do I use this??” 🙃 But I didn’t know about the universe mvar helpers, that’s very useful!)

[Jannis Limperg]

Kyle Miller said:

it seems like it's usually written as mkConst

This is a relic from the dark days before @[computed_field], when the Expr constructors were forbidden. Now .const is again the preferred spelling.