nLab
inductive definition

Contents

Idea

An inductive definition is a definition by induction/recursion.

Definition

See at inductive type.

References

A textbook account is in section I.2 of