精益有签名声明的语法吗？

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

（来自 Theorem Proving in Lean）

精益有签名声明的语法吗？

Does lean have syntax for declaration of signatures?

lean