Documentation

Lean.Meta.BinderNameHint

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

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

Equations
    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
        Instances For
          source
          partial def Lean.Expr.resolveBinderNameHint.go (e : Expr) :
          MonadCacheT ExprStructEq Expr (StateT (Array Name) CoreM) Expr