lean有签名声明的语法吗?

我已经看过了,但还没有找到文档中描述的任何机制,它允许您通过签名来描述一个部分。例如,在下面的部分中,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