Concept
Rocq inductive definition
Journey Statuslearning
It allows defining Algebraic data types in Rocq, including Recursive types.
Its name bears resemblance to Inductive definition.
It allows defining Algebraic data types in Rocq, including Recursive types.
Its name bears resemblance to Inductive definition.