3.5. Recursive Definitions

3.5.1. Structural Recursion

Planned Content

This section will describe the specification of the translation to recursors.

Tracked at issue #55

3.5.1.1. Mutual Structural Recursion

Planned Content

This section will describe the specification of the translation to recursors.

Tracked at issue #56

3.5.2. Well-Founded Recursion🔗

Planned Content

This section will describe the translation of well-founded recursion.

Tracked at issue #57

3.5.3. Controlling Reduction

Planned Content

This section will describe reducibility: reducible, semi-reducible, and irreducible definitions.

Tracked at issue #58

3.5.4. Partial and Unsafe Recursive Definitions🔗

Planned Content

This section will describe partial and unsafe definitions:

  • Interaction with the kernel and elaborator

  • What guarantees are there, and what aren't there?

  • How to bridge from unsafe to safe code?

Tracked at issue #59