5.1. Mutual Recursion🔗

Just as a recursive definition is one that mentions the name being defined in the body of the definition, mutually recursive definitions are definitions that may be recursive or mention one another. To use mutual recursion between multiple declarations, they must be placed in a mutual block.

syntaxMutual Declaration Blocks

The general syntax for mutual recursion is:

command ::= ...
    | mutual
        declaration*
      end

where the declarations must be definitions or theorems.

The declarations in a mutual block are not in scope in each others' signatures, but they are in scope in each others' bodies. Even though the names are not in scope in signatures, they will not be inserted as auto-bound implicit parameters.

Mutual Block Scope

Names defined in a mutual block are not in scope in each others' signatures.

mutual
  abbrev NaturalNum : Type := Nat
  def n : unknown identifier 'NaturalNum'NaturalNum := 5
end

unknown identifier 'NaturalNum'

Without the mutual block, the definition succeeds:

abbrev NaturalNum : Type := Nat
def n : NaturalNum := 5

Mutual Block Scope and Automatic Implicit Parameters

Names defined in a mutual block are not in scope in each others' signatures. Nonetheless, they cannot be used as automatic implicit parameters:

mutual
  abbrev α : Type := Nat
  def identity (x : unknown identifier 'α'α) : unknown identifier 'α'α := x
end

unknown identifier 'α'

With a different name, the implicit parameter is automatically added:

mutual
  abbrev α : Type := Nat
  def identity (x : β) : β := x
end

Elaborating recursive definitions always occurs at the granularity of mutual blocks, as if there were a singleton mutual block around every declaration that is not itself part of such a block. Local definitions introduced via Lean.Parser.Term.letrec : termlet rec and Lean.Parser.Command.declaration : commandwhere are lifted out of their context, introducing parameters for captured free variables as necessary, and treated as if they were separate definitions within the Lean.Parser.Command.mutual : commandmutual block as well. Explain this mechanism in more detail, here or in the term section. Thus, helpers defined in a Lean.Parser.Command.declaration : commandwhere block may use mutual recursion both with one another and with the definition in which they occur, but they may not mention each other in their type signatures.

After the first step of elaboration, in which definitions are still recursive, and before translating recursion using the techniques above, Lean identifies the actually (mutually) recursive cliquesdefine this term, it's useful among the definitions in the mutual block and processes them separately and in dependency order.