Get projection functions for constructors

Stream: Is there code for X?

[Jeremy Salwen]

In Lean4 metaprogramming, is there a way to get the functions which project onto the constructor's arguments?

e.g. for the Fin.mk constructor, getting the Fin.val and Fin.isLt functions?

I tried looking at ConstructorVal to get the names of the arguments and find the definitons that way, but ConstructorVal only has numFields which gives the number of fields, but not their individual names.

[Mario Carneiro]

the InductiveVal has the constructor names

[Jeremy Salwen]

I think that is the name of the constructor, but not the names of the fields in each constructor? i.e.. I can get the list of constructors [mk] but not the list of fields [val, isLt]

[Jeremy Salwen]

I found this code which I think suggests I am just looking for Expr.proj: https://github.com/leanprover/lean4/commit/d685c545b46b5d026475789d77be031bfb64f88d#diff-ef04fb1f36d5ff09309ce70c34e097c76cf70f311d8eeff1df65a00d7b36b0d7R22

What is the relationship between (mkApp2 ``Fin.val 10 a) and (.proj ``Fin 0 (mkApp ``Fin 10))? Are they identical, or does one reduce to the other or is a wrapper for the other?

[Jeremy Salwen]

Hmm, I seem to be able to create expressions using Expr.proj, like the following:

∀ {x : Fin}, { val := x.1, isLt := x.2 } = Fin.ofNat ↑(Fin.ofNat 0)

But I don't think it's well formed. The lean infoview warns me Error: Rpc error: InternalError: invalid projection x.1. I am guessing that x.1 is not a valid substitute for x.val?