Skip to content
scrambled
Programming Language Theory Flashcard

How to define recursive functions in rocq?

Books Concepts Deckrocq-programming-language

Question

How to define recursive functions in rocq?

Answer

Use the Fixpoint definition. For example:

coq
Fixpoint even (n : nat) : bool :=
	match n with
		| O => true
		| S O => false
		| S (S n') => even n'
	end.