source
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

Instances For

source
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' #[]

Instances For