Stream: Coq users

Topic: Is forward declaration possible in coq?

Julin S (Sep 18 2021 at 06:26):

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?

Théo Winterhalter (Sep 18 2021 at 06:53):

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: Oct 13 2024 at 01:02 UTC