inductive

Documentation

Overview

Example inductive demonstrates inductive types and their eliminators.

This example shows how to:

• Define and use inductive types (Nat, Bool)
• Use eliminators (recursors) for dependent elimination
• Compute with inductive types via NbE
• Understand the structure of recursor types

Inductive types are the foundation of dependent type theory, providing a way to define datatypes with guaranteed termination through structural recursion.