Does lean have syntax for declaration of signatures?

Question

I've looked but haven't found any mechanism described in the documentation which allows you to describe a section by it's signature. For example, in the section below the syntax of def requires the right hand side (here sorry)

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

Is there anything like a signature which would allow you to forward declare the contents of a section? Such as in the following made up syntax.

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

The closest i've come using actual syntax is the following, which declares the proofs twice, the second time for keeping the proof on the right hand side as short as possible.

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

No, forward declarations are not allowed in general. Lean, like most other ITPs, relies on the order of declarations for termination checking. Forward declarations would allow you to introduce arbitrary mutual recursion, which Lean 3 only accepts in a clearly delimited context:

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

(from Theorem Proving in Lean)