coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Problems with ignored notations

From: Sebastian Böhne <boehne AT uni-potsdam.de>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Problems with ignored notations
Date: Fri, 10 Feb 2017 12:41:52 +0100
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=boehne AT uni-potsdam.de; spf=Pass smtp.mailfrom=boehne AT uni-potsdam.de; spf=None smtp.helo=postmaster AT cl-mail.uni-potsdam.de
Ironport-phdr: 9a23:EGDIoxMKkd61YwZBEvQl6mtUPXoX/o7sNwtQ0KIMzox0Lfj7rarrMEGX3/hxlliBBdydsKMYzbqJ+Pq9EUU7or+5+EgYd5JNUxJXwe43pCcHRPC/NEvgMfTxZDY7FskRHHVs/nW8LFQHUJ2mPw6arXK99yMdFQviPgRpOOv1BpTSj8Oq3Oyu5pHfeQtFiT6ybL9oLxi7rwrdutcWjIB/Nqs/1xzFr2dSde9L321oP1WTnxj95se04pFu9jlbtuwi+cBdT6j0Zrw0QrNEAjsoNWA1/9DrugLYTQST/HscU34ZnQRODgPY8Rz1RJbxsi/9tupgxCmXOND9QL4oVTi+6apgVRnlgzoFOTEk6mHakst+gr9UrxyhpRN/zZDabo+WOvVica3QZs8aSGlbU8pNTSFNHoGxYo0SBOQBJ+ZYqIz9qkMToxSgHgajHvjvyiNJhnDs260xzvksCQfG3AwmAd0FrXPZo87yNKgMUeC1yrfHwC7eb/NQ2Dfx8ZDIchc9ofGXQL1/a8/RxVMyGAzbl1idr5HuMTCN1ukVrmSW4PdsWfishmMjsQ18ozuiyt0xhoXRm44YxU3I+T96zYsxP9G0VU52bN++HJdOqy2WKo17Sd44TW5yoiY10LgGtIa7fCcUzJQnwAbSZOCDc4SR5xLsTueRITNiiHJ4frK/hg++8VCnyu3gTcm7zUxFri9fntbRqH8Bzx3T6s6ZRfth5kqtxDmC2x3J5uxHJU04j6vWJp07zrItjpYTtF7MHi7ymEX4lq+WcUAk9/Cz5OTgfLrmppmcOJFvhwHjNKQum9WzAfw/MggSRGiU5P6z1Lj58ULkXrpGluc2nbXBsJDGOcQboba0DBNS0oY68hqwEzOm0MkDknQcN1JEeBeHj5DzNF3UIfD4C+2/g1W2nztxyfDGJO6pPpKYJX/a1bzlYLxV6khGyQN1w8oMyYhTD+Q6Lfj6QVPwvdqQJIE5NQH8l+zgBdV726sDX2PKGqiFK6/btBmE67R8cKG3eIYJtWOleLAe7Pn0gCphlA==

Dear Coq-community!

Thank you all very much for your help!

The solution with leaving ": ℤ" indeed works perfectly. We never would have thought that this could be a problem. So again, thank you very much!

The approach with typeclasses seems to be different but very interesting, too. Thank you, Abhishek, for the links. We will definitely have a look at it.

Best regards

Tim Richter and Sebastian Böhne

[Coq-Club] Problems with ignored notations, Sebastian Böhne, 02/09/2017
- Re: [Coq-Club] Problems with ignored notations, Gaetan Gilbert, 02/09/2017
  - Re: [Coq-Club] Problems with ignored notations, Guillaume Melquiond, 02/09/2017
    - Re: [Coq-Club] Problems with ignored notations, Sebastian Böhne, 02/10/2017
- Re: [Coq-Club] Problems with ignored notations, Abhishek Anand, 02/09/2017
  - Re: [Coq-Club] Problems with ignored notations, Abhishek Anand, 02/09/2017