Concept
Inductive type
Journey Statusreviewing Tags
Tools: Rocq (formerly Coq)
INFO
(Type theory, Formal system) A type defined by a finite set of Constructors that specify all possible ways to build its values, enabling Pattern matching and Structural recursion (like nat, list, or tree).