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

#### 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!

• I couldn't reproduce this. I copied your file structure and defined leb as expected. The main difference was that I also added a Makefile (this one, that I copied from somewhere but I don't remember where) and included the file names in the _CoqProject so that make could compile everything. Then I obtained the expected outputs in Structures.v, not the ones you did. Question: what happens when you Compute and Print in Types.v? Are you sure this is related to doing it on a different file? Jun 1 at 10:54
• Thanks, Compute and Print are indeed working fine in Types.v. Jun 1 at 11:16

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.

• Thanks! Indeed your guess is right, after compiling Types.v and Recursion.v again, now the function can be used normally in Structures.v. Jun 1 at 11:23
• Not sure why, I thought Proof General will auto compile some .v files on demand. because when I'm just getting started yesterday, I started seeing .vo being produced without me invoking any command. Jun 1 at 11:25
• Another solution is to make clean and make build again. Jun 1 at 11:26