Stream: Coq users

Topic: Error: not found in table: core.JMeq.type


view this post on Zulip Lef Ioannidis (Jun 09 2021 at 01:36):

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?

view this post on Zulip Lef Ioannidis (Jun 09 2021 at 01:49):

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?

view this post on Zulip Matthieu Sozeau (Jun 09 2021 at 10:29):

You can look into the documentation of Program and the JMeq file in the standard library to get more information


Last updated: Feb 06 2023 at 11:03 UTC