lean - 精益是否有声明签名的语法？

Question

我已经查看但没有找到文档中描述的任何机制，它允许您通过其签名来描述一个部分。例如，在下面的部分中，def 的语法需要右手边（这里很抱歉）

section
  variable A : Type
  def ident : A → A := sorry
end

有没有类似签名的东西可以让你转发声明一个部分的内容？比如下面的组成语法。

signature
  variable A : Type
  def ident : A → A
end

我使用实际语法最接近的是以下，它声明了两次证明，第二次是为了使右侧的证明尽可能短。

section
  variables A B : Type
  def ident' {A : Type} : A → A := (λ x, x)
  def mp' {A B : Type}: (A → B) → A → B := (λ f, λ x, f x)

  /- Signature-/
  def ident : A → A := ident'
  def mp : (A → B) → A → B := mp'
end

Answer 1

不，一般不允许前向声明。与大多数其他 ITP 一样，精益依赖于声明的顺序来进行终止检查。前向声明将允许您引入任意相互递归，精益 3 仅在明确界定的上下文中接受：

mutual def even, odd
with even : nat → bool
| 0     := tt
| (a+1) := odd a
with odd : nat → bool
| 0     := ff
| (a+1) := even a

（来自精益中的定理证明）