Concept

Function rocq

Modified just now

Journey Statuslearning

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.