Hi.

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 [5] 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: Sep 26 2023 at 12:02 UTC