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!