14.7. 命名绑定变量🔗

当简化器或 rw 策略引入函数参数等新的绑定形式时，会根据所应用重写规则的陈述中的名称，为绑定变量选择名称。 必要时会使该名称保持唯一。 在某些情况下，例如为使用良基递归的终止性证明预处理定义时，终止性证明义务中出现的名称应当是原函数定义中写下的对应名称。

binderNameHint 小工具可用于指示：应根据其他某个项中绑定的变量来命名一个绑定变量。 按照约定，项 () 用于表示名称不应取自原定义。

binderNameHint.{u, v, w} {α : Sort u} {β : Sort v} {γ : Sort w} (v : α)
  (binder : β) (e : γ) : γ
binderNameHint.{u, v, w} {α : Sort u}
  {β : Sort v} {γ : Sort w} (v : α)
  (binder : β) (e : γ) : γ