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
computes to itself:
Compute (leb 2 3).
= leb 2 3 : bool
*** [ leb : nat -> nat -> bool ] Arguments leb (n m)%nat_scope
- Why does
lebexpands to itself?
- What does
*** [ leb : nat -> nat -> bool ]mean with
- How to make
Structures.v, such that I can use
Types.vwhere it is defined?