coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: Xuanrui Qi <xqi01 AT cs.tufts.edu>
To: coq-club AT inria.fr
Subject: [Coq-Club] Debugging "unable to build a covering" errors in Equations
Date: Fri, 14 Jun 2019 21:32:21 -0700
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=xqi01 AT cs.tufts.edu; spf=Pass smtp.mailfrom=xqi01 AT cs.tufts.edu; spf=None smtp.helo=postmaster AT vm-delivery1.eecs.tufts.edu
Ironport-phdr: 9a23:M5uBChd6VSVfIFTt/jZpvyP2lGMj4u6mDksu8pMizoh2WeGdxcu4ZR7h7PlgxGXEQZ/co6odzbaP6ua5BzZLsczJmUtBWaQEbwUCh8QSkl5oK+++Imq/EsTXaTcnFt9JTl5v8iLzG0FUHMHjew+a+SXqvnYdFRrlKAV6OPn+FJLMgMSrzeCy/IDYbxlViDanbr5+MQi6oR/MusQXn4duJaU8xgXUqXZUZupawn9lK0iOlBjm/Mew+5Bj8yVUu/0/8sNLTLv3caclQ7FGFToqK2866tHluhnFVguP+2ATUn4KnRpSAgjK9w/1U5HsuSbnrOV92S2aPcrrTbAoXDmp8qlmRAP0hCoBKjU09nzchM5tg6JBuB+vpAFxzY7Kbo+bKPVxcKzSc9wBSGpdXMtcTTBNDp+mYoYNCecKIOZWr5P6p1sLtRaxBBSsC/npyj9Sm3/23LAx3f8gEQrb2wEhEMsOsHXIoNnoL6odTfu1wLPUzTXeYfNWxSz95JLWfR88vPGBRLR9etfSx0k3Dw7Jk1udpZD/Mz6U2ekBqXaX4uR6We+hiWMrswB8rzq1yssyloXEhJgZxk3a+Sh32oo5OMO0RUhmatC+CpRQrTuVN45uT8MiXW5ovCE6x6UYuZ6+ZSQF1Yooxxrea/yZbYeI+BLiWPuLLThmmn1qZKm/iwyu8Ui9xO38StK03ExUoSVYj9nArnEN1xrN5cibUvZx40ms1SqV2w3S5exIO144mKTBJ5MvwLM8jp8Tvl7CHi/ylkX2lqiWdkA89+mn8uTnY6nqqoKHOoBokQHyKLgumtGxAeQkKQgCRXaU9vmh1LH75032XK1KjuEqkqneqJ3VOcMbpregDwBJ1oYj9g2wAiy90NUYmHkHNEhKdAiGj4jvIVHOIer3Ae2xg1S2w39XwKXNOaSkCZHQJFDClq3gdPBz8R1y0g02mOBC7pROF7BJGfO7Dl/otYSBJhQidRCpzfr8Tthxy9VNCiq0HqaFPfaK4hez7eU1LrzUPdJHiHPGM/EgosXWozo5lFsaJ/j7w55SZH28H+prOVTAJ3fhicxHDXoEohF4QeD32gXbAGxjIk2qVqd53QkVTYevDIPNXIeo2eDT1zz9AoBYensAB1yRQy6xK9e0HswUYSfXGfdP1yQeXOH9GYQ6kw2zuhPhjbdrM7iM9w==

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

[Coq-Club] Debugging "unable to build a covering" errors in Equations, Xuanrui Qi, 06/15/2019
- <Possible follow-up(s)>
- Re: [Coq-Club] Debugging "unable to build a covering" errors in Equations, Jason -Zhong Sheng- Hu, 06/15/2019