coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] "check_not_nested" error with Function

From: Timothée Defourné <tdefourne AT clipper.ens.fr>
To: coq-club AT inria.fr
Cc: Bruno Grenet <bruno.grenet AT lirmm.fr>
Subject: [Coq-Club] "check_not_nested" error with Function
Date: Wed, 22 Jul 2020 13:42:59 +0200
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=tdefourne AT clipper.ens.fr; spf=Pass smtp.mailfrom=tdefourne AT clipper.ens.fr; spf=None smtp.helo=postmaster AT nef.ens.fr
Ironport-phdr: 9a23:Pbig8BeqjxFdOtPGyFdbmiE9lGMj4u6mDksu8pMizoh2WeGdxcW6Yh7h7PlgxGXEQZ/co6odzbaP7ea8CCdcuN6oizMrSNR0TRgLiMEbzUQLIfWuLgnFFsPsdDEwB89YVVVorDmROElRH9viNRWJ+iXhpTEdFQ/iOgVrO+/7BpDdj9it1+C15pbffxhEiCCybL9vLRi6twrcu80ZjYZtN6o61wfErGZPd+lK321jOEidnwz75se+/Z5j9zpftvc8/MNeUqv0Yro1Q6VAADspL2466svrtQLeTQSU/XsTTn8WkhtTDAfb6hzxQ4r8vTH7tup53ymaINH2QLUpUjms86tnVBnlgzocOjUn7G/YlNB/jKNDoBKguRN/xZLUYJqIP/Z6Z6/RYM8WSXZEUstXSidPAJ6zb5EXAuQcM+ZWsYnzqVgAoxSwCgajBv/gxDBTi3/q3qA3yfgtHR3I0QEiGd8FrXTarM/yNKcXSe270qjIzTDEb/NK2Tf68pbHfQgvr/6SU7JwdtfRyVMpFwTfk16drpDlMC6L2eQDtGib8vBgVeSxhGM8tw5xpjmvxt80iobXnIIZ0E7L9SNiwIovK924Uld2bNi5G5Rfqy+ULZF5Qt8+Q252oiY6zKULtJClcSUIyJopxwPTZ+Gbf4aG4hzuSuafLDZ3iX9rd7yzmhe//Eahx+DyWcS4zVRHojRZn9fDuH0A1BPe58eaRvZ740yv1zGP1wXJ5eFFJ0A5javbK5suwr4tjJofq1jMHijzmEjwkaSYdV0k9/C15+j5ZrjqvIKQOotwhw3kNqkjm9azDOskPgQWQmSX5+Cx2Kf+8UD9RLhGlOA6nrPHvJzEI8kQu7S3DBVP0ok57hayFzem38ocnXkANF9FfgyIj4bzN17QJvD4Fu2zg1q2kDtzxvDGOKPuAonVI3Tejrvseaxx51NYxQc319xS45NZBqsOLf7vQkPxscbXDh49Mwy62ebnD9B925sCWW2SHKCZPqTSsUKS5uIpPeaBf5MauDL8K/g9//7hk2U5lUUDcqmvxpsbcn64Hu5+L0WDfXXsmssBEXsNvgcmUOPqj0SCXSdPaHa2QqIz/So2CJmmDIfGXoCimqaN3Ca9Hp1MZ2BJEEqAEXnyd9bMZ/BZYyWLZ8RljzYsVL67SoZn2wv9mhX9zu9bL+/T5i2ZuKXP2dZy+vfVFFlm6TB5AcOAyWeAZ2pwn3sQSiVw0aZk50JnnATQmZNkiuBVQIQAr8hCVR03YNuFl7QjWoLCHznZd9LMc26IB9CvADU/VNU0moFcaEJ8A82vlFbO2THsDaVHzuXXVqxxybrV2j3KH+g402zPjfdzhF0nWtNCLyurgLU5+RKBX9eUwXXcrL6jcOEn5ACI9GqHyjPU7kdVXkh9V76DU2pNPkY=

Hello,

I'm having an issue I don't understand with Coqtail, in the following function defined with the Function command : https://i.imgur.com/sW3EYLG.png

I get the error : on expr : quo (ceiling (NQ_div2 (deg R0))) R0 check_not_nested: failure R0, from the recursive call in the highlighted line.

I have never seen this error before and researching it yields no result. Does anyone have an idea what it means ? I believe I can work out what exactly went wrong if I just know what the error means.

Also, if it helps, making the function end immediately after the highlighted line raises no error, but ending it after the second pattern matching raises the same error.

Thanks in advance,

Timothée Defourné

[Coq-Club] "check_not_nested" error with Function, Timothée Defourné, 07/22/2020