Programming Language Theory Flashcard
How to define a tuple type in rocq?
Books
Concepts
Deckrocq-programming-language
Question
How to define a tuple type in rocq?
Answer
Multiple fields inside a constructor.
coq
Inductive nybble : Type :=
| bits (b1 b2 b3 b4 : bit)