Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] Debugging "unable to build a covering" errors in Equations

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Debugging "unable to build a covering" errors in Equations


Chronological Thread 
  • From: Jason -Zhong Sheng- Hu <fdhzs2010 AT hotmail.com>
  • To: "coq-club AT inria.fr" <coq-club AT inria.fr>
  • Subject: Re: [Coq-Club] Debugging "unable to build a covering" errors in Equations
  • Date: Sat, 15 Jun 2019 10:47:08 +0000
  • Accept-language: en-CA, en-US
  • Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=fdhzs2010 AT hotmail.com; spf=Pass smtp.mailfrom=fdhzs2010 AT hotmail.com; spf=Pass smtp.helo=postmaster AT NAM02-BL2-obe.outbound.protection.outlook.com
  • Ironport-phdr: 9a23:nJ/MLBVDPHuNY3/uLIRtm0gwQuDV8LGtZVwlr6E/grcLSJyIuqrYbBCDt8tkgFKBZ4jH8fUM07OQ7/m5HzVeut3b4TgrS99lb1c9k8IYnggtUoauKHbQC7rUVRE8B9lIT1R//nu2YgB/Ecf6YEDO8DXptWZBUhrwOhBoKevrB4Xck9q41/yo+53Ufg5EmCexbal9IRmrsAndrNQajIpsJ6o+1BfEpmZDdvhLy29vOV+dhQv36N2q/J5k/SRQuvYh+NBFXK7nYak2TqFWASo/PWwt68LlqRfMTQ2U5nsBSWoWiQZHAxLE7B7hQJj8tDbxu/dn1ymbOc32Sq00WSin4qx2RhLklDsLOjgk+2zRl8d+jr9UoAi5qhJ/3YDafZ2VOvR9cKzBctwXXnBOUtpNWyFbHo+wc4kCAuwcNuhYtYn9oF4OoAO6Cwa2H+PvzTlIjWLv0aI50+QhFgfG3AM9FNwTsHTbstP1NKgLXeuozqfI0CjIYvRY2Tjg6IjJcwshre+QUb5tbcbc0kkvFwTZjlWVs4PlPjeV2v4RvGic6uptTOSigHMkpQFpujWiydsghpPNi44L0FzJ+z91zYUxKNGgRk50f92pHIdVuiyfN4Z7TcEvTmNttSs017IJp4W0cS0Xx5koyRPSZfmKfoqU7hLtSOqcJypzimh/d7KlnRmy9FCtyu3iWcmw11ZHtjJLn8XLuHwRyRDf89WKRP1j8ku43jaAzB7c5vtDIUApiarUMJkhwqM2lpUOq0jDBjX2mELqjKCIakok5umo6+PhYrn8oZ+cKpN0igX5MqQpmcyzG/g3Mg8LX2SD+OS80qPs/VHhTbhFkvE6iK3UvI7AKckVvKK0AAtY3p4m6xmlDjem1NoYnWMALFJAYB+HgZXmO1HPIfDjE/uzn0mgnCtwyvDGOb3hHpDNIWLCkLflZ7py90lcyA8rwdBF+51UEq0BIO70WkLpqNPYCQY5PxWozObjFdVyzZgTWXmPA6+cKKPdq0WE5uMpI+mWZY8aoizxK/Y/562msXhs01QaZOyi2YYdQHG+BPVvZUuDKzK4idAYVGwOowAWTerwiVTEXyQFNFioWKdpxDggD4TuSLXDQYaiyIeB0SG0W9V2eygSBFyMA2yyL9zcc/cLdCebI8snmTsBA+vyA7Q93A2j4Vepg4FsKfDZr3VB5MDTkeNt7uiWrikcsDl9DsCTyWaIFjomnmQUQjY32OZ0pkkvkw7eg5g9uORREJlo390MUgo+MsKDncpTLoioHyjlJJKOQlvgRci6CzYsSN5328UJf0t2B9SliFbEwjauBLgW0beMAc5tq/6O7z3KP894jk3++uw5lVB/GZlPMnGjj697sQPUAtyRng==

Hi Xuanrui,

I believe the second line of the error message shows you at least one of the cases that you missed.

Thanks,
Jason Hu

On Jun 15, 2019 00:32, Xuanrui Qi <xqi01 AT cs.tufts.edu> wrote:
Dear Coq-Clubbers,

I have some Agda code that I want to translate to Coq using Equations.
I transcribe the pattern-matching clauses as-is, and Equations fails
with a mysterious message:

Unable to build a covering for:
balright d cl cr c l v r valid_l valid_r

which I assume to be indicative of missing cases. However, it doesn't
tell me what clauses are missing specifically. How would I trace down
the error in this case and add the proper impossible clauses?

Best,
Xuanrui





Archive powered by MHonArc 2.6.18.

Top of Page