proj to const

Stream: metaprogramming / tactics

[Chase Norman]

Expr.lean says

“When exporting Lean developments to other systems, proj can be replaced with typeName.rec
applications.”

Is there a function that does this?