def Lean.Expr.hasBinderNameHint (e : Expr) : Bool

Does e have a binder name hint? (quick check)

Equations

• e.hasBinderNameHint = (Lean.Expr.find? (fun (e : Lean.Expr) => e.isConstOf `binderNameHint) e).isSome

def Lean.Expr.resolveBinderNameHint (e : Expr) : CoreM Expr

Resolves occurrences of binderNameHint in e. See docstring of binderNameHint for more information.

Equations

• e.resolveBinderNameHint = (Lean.Expr.resolveBinderNameHint.go e).run.run' #[]

partial def Lean.Expr.resolveBinderNameHint.go (e : Expr) : MonadCacheT ExprStructEq Expr (StateT (Array Name) CoreM) Expr