coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Patricia Peratto <psperatto AT vera.com.uy>
- To: coq-club <coq-club AT inria.fr>
- Subject: [Coq-Club] question about as
- Date: Mon, 17 May 2021 15:39:57 -0300 (UYT)
- Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=psperatto AT vera.com.uy; spf=Pass smtp.mailfrom=psperatto AT vera.com.uy; spf=None smtp.helo=postmaster AT mail.vera.com.uy
- Dkim-filter: OpenDKIM Filter v2.9.0 mta02.in.vera.com.uy 367CD222593
- Ironport-hdrordr: A9a23:KNrBPaqBKCA1Aw19MckMGaIaV5o2eYIsimQD101hICG9JPb3qynIppQmPHDP+VQssRsb8+xoVJPwJE80lqQV3WBuB8bAYOCOggLBR+xfBODZrAEIdReTytJg
- Ironport-phdr: A9a23:YtCGkBee0FVm4ac2wAbxLxK7lGM+V97LVj580XLHo4xHfqnrxZn+JkuXvawr0AaYG9+Ftrkd0raempujcFRI2YyGvnEGfc4EfD4+ouJSoTYdBtWYA1bwNv/gYn9yNs1DUFh44yPzahANS47xaFLIv3K98yMZFAnhOgppPOT1HZPZg9iq2+yo9JDffgFFiCCjbb5zLBi6ohjdutQZjIB/Nqs/1xzFr2dSde9L321oP1WTnxj95se04pFu9jlbtuwi+cBdT6j0Zrw0QrNEAjsoNWA1/9DrugLYTQST/HscU34ZnQRODgPY8Rz1RJbxsi/9tupgxCmXOND9QL4oVTi+6apgVRnlgzoFOTEk6mHaksJ+gqJFrhyipRNx3oHbb52UNPpiZa7SZ88WSnZaUcpNSyBMAIWxZJYPAeobOuZYqpHwqUEUohuiHwmsBf/gyj5SiXTrx6M1zf4hHhva3Aw8GNIFrXPZrM3uNKcKT++11rPHzSnfb/NRwjr99pbHcgo7rv2WQb1wds/RxVMyFwLFl1idr5HuMDyJ2OoXqWeb8/ZgWvy1i24hswx8oiaiytojhIfJiY8Y1EzI+CR9zYopK9C2RlN3bcC4HJVQtiyUN497Tt08T2xmpio3yrIItJ2mcSUXypkqxwPSZvqaeIaL+hLuTPidLStkiH5/d7+zmwy+/Ea9xuHmWcS50E5GojdHn9XSrHwByRPe5tKJR/dg5Eus1yiD2gbO4e9eO080j7DUK5s5z74wiJUTtUPDEzfzmErsja+Wcl8o+va25OT9eLrqvIOTN4hxig3kL6QvmtSzAeU+MgcQQ2iW4fqw2KH/8UHjT7hGkuc6n6fEvJzAKskWpra1AwpP3YYi7xa/AS2m0NMdnXQfNFJFYwqHgJbzO17UPPD4EfC/jk+ykDh13fDJJKftDYnKLnjGirvhYLZ851ZGyAUv1dBf+45UCrYZLf3vXU/xrcXUAQM9Mwyp2OnqE85914MbWWKXGKCVKqLSsVmS5uIuOeaAfoEVuCyuY8QisvXplDoynUIXNf2i2oJSY3SlFNxnJV+YaDzimIFSP30Nu18GRfDwiVaDWHZramy7Q747rmUjE5qrF47fWoeFnrGb1WGwGZgQe3EQWQPEKmvha4jRA6REUymVOMI0ylTssJC/RpUokxqpsUnn2ug/RgI70jMVr5ul399wofDCx0haHd1cCs2c1yeTQnt92GgPQnkrzfInyXE=
I have proved :
Theorem neq_nil_cons2 (A:Type(x:A)(y:list A): not (cons x y =nil).
I need to use neq_nil_cons2 in a recursive call of a fixpoint.
| x :: (y :: s) as ys => ........neq_nil_cons2 A y s...........
but coq asks me to apply the function to ys.
How I can do this?
Patricia
- [Coq-Club] question about as, Patricia Peratto, 05/17/2021
Archive powered by MHonArc 2.6.19+.