Cannot coerce aeval to an evaluable reference

Using Coq
1

Hi! I have got this code:

Fixpoint aeval (ex:aexp) (st:M.t Z) : Z :=
  match ex with
...
  end.

Lemma executeCompile aeval : ...
Proof.
...
      unfold aeval.

But when I do unfold aeval. I get the error “Cannot coerce aeval to an evaluable reference”.
Why does this happen? How can I fix it? Thank you!

2

aeval is a universally-quantified variable of your lemma. It is not the aforementioned fixpoint function.

2 Likes