Programming Language Theory Flashcard

How to define an enumerated type in rocq?

Books

Concepts

Deckrocq-programming-language

Question

How to define an enumerated type in rocq?

Answer

Use the Inductive keyword:

coq

Inductive nat : Type :=
	| O
	| S (n : nat).