Stream: Coq users

Topic: Is forward declaration possible in coq?


view this post on Zulip 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?

view this post on Zulip 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: Feb 04 2023 at 21:02 UTC