Is it possible to have 'forward declarations' in coq?
So that we can use a function even before its definition appears in the coq source file?
To make stuff like this (just a toy example):
Definition foo (n : nat) : nat := (* Apply [bar] on zero. Return same value otherwise. *) match n with | O => bar n | _ => n end. Definition bar (n : nat) : nat := (* Apply [foo] on non-zero. Return  otherwise. *) match n with | O => 5 | _ => foo n end.
where the function
bar is used in
foo even before its definition is evaluated.
Is this possible in coq?
It sounds like you want to do mutual definitions. See https://coq.inria.fr/refman/language/core/inductive.html (Example: Mutual fixpoints) for instance.
Last updated: Feb 04 2023 at 21:02 UTC