Replacing `.proj` with `.rec`

Stream: Is there code for X?

[Eric Paul]

It is mentioned in the doc string for docs#Lean.Expr.proj that it can be replaced by an application of the type's recursor. I was hoping to do that replacement. Has someone already written code to do this somewhere?

[Kenny Lau]

Welp I thought Lean.Meta.reduceProj? would do that but I couldn't get it to work :melt:

[Aaron Liu]

#Is there code for X? > Converting Expr projection to recursor application @ 💬

[Eric Paul]

Oh great, thanks! I hadn't found that

[Kenny Lau]

Kenny Lau said:

Welp I thought Lean.Meta.reduceProj? would do that but I couldn't get it to work :melt:

aha i figured out why, it's supposed to work with expressions like (.mk ..).1, not just foo.1