3.16. Sections

It often happens that a couple of declarations need the same arguments. Then these declarations can be put into a section.

Syntax:

section <telescope> :=
    <declaration₁>
    <declaration₂>
    ...

The telescope defines the common arguments for the declarations. If a declaration does not need an argument, that argument is not included in the final declaration.

Example:

section {A: Any} :=
    (+): List A → List A → List A := case
        \ [] b :=
            b
        \ (h :: t) b :=
            h :: t + b

    reverse: List A → List A := case
        \ [] :=
            []
        \ (h :: t) :=
            reverse t + [h]