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!