Programming Language Theory Flashcard
What does an inductive definition in rocq do?
Books
Concepts
Deckrocq-programming-language
Question
What does an inductive definition in rocq do?
Answer
It allows defining Algebraic data types in Rocq, including Recursive types.
Its name bears resemblance to Inductive definition.