←Prev ↑Up Next→

The Lean Language Reference

1.	Introduction
2.	Elaboration and Compilation
3.	The Type System
4.	Source Files
5.	Recursive Definitions
6.	Terms
7.	Type Classes
8.	Functors, Monads and `do`-Notation
9.	IO
10.	Tactic Proofs
11.	The Simplifier
12.	Basic Types
13.	Standard Library
14.	Notations and Macros
15.	Output from Lean
16.	Elan
17.	Lake and Reservoir
	Index

5. Recursive Definitions

5.1.	Mutual Recursion
5.2.	Structural Recursion
5.3.	Well-Founded Recursion
5.4.	Partial and Unsafe Recursive Definitions
5.5.	Controlling Reduction

5.5. Controlling Reduction

Source Code
Report Issues

5.5. Controlling Reduction

Planned Content

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

Tracked at issue #58