PROSAGA码农传奇-精益-为什么类型类和隐式参数机制？

<div class =“post-text”itemprop =“text”>
  <P>
    Lean的elaborator会自动插入隐式参数。该
     <code>
      {x : Type}
    </code>
     出现在两个定义中的是一个隐含参数的例子：如果有的话
     <code>
      s : inhabited nat
    </code>
    ，那你就可以写了
     <code>
      foo s
    </code>
    ，这将详细说明一个类型的术语
     <code>
      nat
    </code>
    ，因为
     <code>
      x
    </code>
     参数可以从中推断出来
     <code>
      s
    </code>
    。
  </p>
  <P>
    类型参数是另一种隐式参数。 elaborator运行一个名为的过程，而不是从后面的参数中推断出来
    <EM>
      类型分辨率
    </EM>
     将尝试生成指定类型的术语。 （见第10章）
    <a href="https://leanprover.github.io/theorem_proving_in_lean/theorem_proving_in_lean.pdf" rel="nofollow noreferrer">
      https://leanprover.github.io/theorem_proving_in_lean/theorem_proving_in_lean.pdf
    </A>
    那么，你的
     <code>
      foo'
    </code>
     实际上根本不会参与任何争论。如果是预期的类型
     <code>
      x
    </code>
     可以从上下文推断，精益会寻找一个实例
     <code>
      inhabited x
    </code>
     并插入它：
  </p>
   <pre>
    <code>
      def foo' {x : Type} [s : inhabited x] : x := default x
instance inh_nat : inhabited nat := ?3?
#eval (2 : ?) + foo' -- 5

</code>
  </pre>
  <P>
    在这里，精益推断
     <code>
      x
    </code>
     一定是
     <code>
      nat
    </code>
    ，并查找并插入实例
     <code>
      inhabited nat
    </code>
    ， 以便
     <code>
      foo'
    </code>
     单独阐述一个类型的术语
     <code>
      nat
    </code>
    。
  </p>
</DIV>