coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Ben Grange <lagrange123 AT gmail.com>
- To: coq-club AT inria.fr
- Subject: [Coq-Club] Field typeclass?
- Date: Tue, 19 Mar 2019 16:46:37 -0400
- Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=lagrange123 AT gmail.com; spf=Pass smtp.mailfrom=lagrange123 AT gmail.com; spf=None smtp.helo=postmaster AT mail-it1-f182.google.com
- Ironport-phdr: 9a23:rBjyYRNTrpbpnd5Baq8l6mtUPXoX/o7sNwtQ0KIMzox0Lfz9rarrMEGX3/hxlliBBdydt6sczbSK+Pm8AyQp2tWoiDg6aptCVhsI2409vjcLJ4q7M3D9N+PgdCcgHc5PBxdP9nC/NlVJSo6lPwWB6nK94iQPFRrhKAF7Ovr6GpLIj8Swyuu+54Dfbx9HiTagfb9+NhS7oAreusULjoZuNLs6xwfUrHdPZ+lY335jK0iJnxb76Mew/Zpj/DpVtvk86cNOUrj0crohQ7BAAzsoL2465MvwtRneVgSP/WcTUn8XkhVTHQfI6gzxU4rrvSv7sup93zSaPdHzQLspVzmu87tnRRn1gyoBKjU38nzYitZoga1UoByvqR9xzZPKbo6JL/dxZL/RcMkASGZdQspcVSpMCZ68YYsVCOoBOP5VopTjqFsIsBCwBBOsC/npyj9HmHD9wKo30+A7HgHJxgwvBdQOsHvKo9noKqsfX/u4zKbNzTrZbvNW3S3x55TPchAkuPyBW697f8nJyUQ3CQ/JklGdpZbmMj6VzOgBrmmW4ut6We6yiGMrtQd8qSW1yMg2kInGnIcVx0jE9SpnxIY1IsW1SEthbt6lFJtcriCaN5drTs87TWFkpSU3xqMctZ60eygKz5snxxrBZPCdb4eI5RfjWP6QITd+mn1lZKqyiwiu/UWk0OHxVcm53ExXoidEk9TArG0B2h/N5sSfT/ty5Eah2TKB1wDJ7eFEJFg5la7BJJ4u2L4/jJwTsUvdESPrhkn7grSbdkoh+uey6uTnZq/qqYObN49xkg3+KLghmtSjAeQkNQgDR3SU+eOl1LH64UL5RKhKgeYtn6nCsJHaINwbqbSjDw9U1IYj8Re/AC283NQWh3lUZG5CLRmAls3iP0zECPH+F/a2xVq2wxlxwPWTFLDnSrrXJ37Mnf+1eb9y8Udaxwdql4t36JddC7VHK/X2DByi/OfEBwM0ZlTni93sD89wg9tHCDC/R5SBOaaXimemo+cmIu2CfogQ4W+vJP0s5vqohng8ywZEIfuZmKAPYXX9JcxIZl2DaCO10NgEGGYO+AE5Sb6y0QDQYXtof3+3GpkEyHQ7BYahV9mRQ4mshPmAwH7+EMQGPCZJDVeDFXqufIKBCa8B
Hi,
I'm going through a linear algebra book (Linear Algebra Done Wrong, for anyone curious), and would like to verify my proofs with Coq. This would involve heavy use of matrices, of course.
I've found the Mathematical Components library, (which has a matrix.v), but this seems like overkill for my humble purposes. Initially, I only went there because I was curious, "how did they implement this kind of polymorphism?" Indeed, what is the best way to quantify over all field-types? Would it be a typeclass? What would be the best way to leverage the existing Coq standard library?
Hopefully this makes sense.
Ben
- [Coq-Club] Field typeclass?, Ben Grange, 03/19/2019
- Re: [Coq-Club] Field typeclass?, Emilio Jesús Gallego Arias, 03/20/2019
Archive powered by MHonArc 2.6.18.