Why does my previously defined function expands/computes to itself?

Question

Problem

I have a function leb defined in one of the (transitively) imported file: Types.v. However, calling it in my current file (Structures.v) doesn't "evaluate" to a value. Instead, it expands to itself, which is unexpected.

To illustrate what I mean, here is the layout of the Coq project directory: (Note: Relevant file content are quoted as strings.)

$PROJECT_ROOT
|- _Coqproject
   "-Q . DMFP"
|- Types.v
   "Fixpoint leb (n m : nat) : bool := ..."
|- Recursion.v
   "Require Export DMFP.Types. ..."
|- Structures.v
   "Require Export DMFP.Recursion. ..."

As you can see, the function leb is defined in Types.v. But when I tried to use it in Structures.v, it computes to itself:

Compute (leb 2 3).

gives this:

     = leb 2 3
     : bool

Then,

Print leb.

gives this:

*** [ leb : nat -> nat -> bool ]

Arguments leb (n m)%nat_scope

Questions

1. Why does leb expands to itself?
2. What does *** [ leb : nat -> nat -> bool ] mean with Print leb.?
3. How to make leb available in Structures.v, such that I can use leb as in Types.v where it is defined?

Thank you!

Answer 1

Your outputs are consistent with leb being defined as a parameter, not as a specific function. So, for example:

Parameter leb : nat -> nat -> bool.

Compute (leb 2 3).
(*     = leb 2 3
     : bool
*)

Print leb.
(*
*** [ leb : nat -> nat -> bool ]

Arguments leb (_ _)%nat_scope
*)

Compare with having an actual definition for leb:

Fixpoint leb (n m : nat) : bool :=
  match n with
  | O => true
  | S k =>
      match m with
      | O => false
      | S k' => leb k k'
      end
  end.

Compute (leb 2 3).
(*
     = true
     : bool
*)

Print leb.
(*
leb = 
fix leb (n m : nat) {struct n} : bool :=
  match n with
  | 0 => true
  | S k => match m with
           | 0 => false
           | S k' => leb k k'
           end
  end
     : nat -> nat -> bool

Arguments leb (n m)%nat_scope
*)

I'm guessing at this point, but here is what could have happened:

1. You stated the existence of leb in Types.v without giving it a definition (eg with Fixpoint leb (n m : nat) : bool. Admitted.)
2. You compiled Types.v
3. You went back to Types.v to fill in your definition of leb
4. You started working on Structures.v without compiling Types.v again, and so it was still using the old version where you hadn't filled in the definition for leb yet.

If this is not what's happening, then please provide more details. As I explained in my comment, I can't reproduce your data.