def Lean.LocalContext.getRoundtrippingUserName? (lctx : Lean.LocalContext) (fvarId : Lean.FVarId) : Option Lean.Name

Given an FVarId, this function returns the corresponding user name, but only if the name can be used to recover the original FVarId.

Equations

• One or more equations did not get rendered due to their size.