Concept
Tuple rocq
Journey Statuslearning
Multiple fields inside a constructor.
coq
Inductive nybble : Type :=
| bits (b1 b2 b3 b4 : bit)Multiple fields inside a constructor.
Inductive nybble : Type :=
| bits (b1 b2 b3 b4 : bit)