Htykuut

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

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)