3.6. Type Classes

Planned Content

This introduction will describe the overall feature.

Tracked at issue #61

3.6.1. Class Declarations

Planned Content

This section will describe the syntax of class and class inductive declarations. The desugaring of class to structure and thus inductive will be addressed, along with the determining of implicitness of method parameters. outParam and semiOutParam will also be described.

Tracked at issue #60

3.6.2. Instance Declarations

Planned Content

This section will describe the syntax of instance declarations, priorities, and names.

Tracked at issue #62

3.6.3. Instance Synthesis

Planned Content

This section will specify the instance synthesis algorithm.

Tracked at issue #63

3.6.4. Deriving Instances

Planned Content

This section will specify syntax of deriving clauses and list the valid places where they may occur. It will also describe deriving instance. It will list the deriving handlers that ship with Lean by default.

Tracked at issue #64

3.6.4.1. Deriving Handlers

Planned Content

This section will describe deriving handlers and how they are invoked.

Tracked at issue #65