Hello, I am trying to define a Program Fixpoint
which looks like a fold over some inductively defined structure. I am getting the following error:
Error: not found in table: core.JMeq.type
. What does this mean?
Looks like Require Import JMeq
will import the JMeq axiom needed and give a different message. Is there anywhere I can read about the differences between eq_rect
and JMeq
?
You can look into the documentation of Program and the JMeq file in the standard library to get more information
Last updated: Oct 13 2024 at 01:02 UTC