coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] More than one ring structure (e.g. modulo ring) for one type

From: e AT x80.org (Emilio Jesús Gallego Arias)
To: Gaetan Gilbert <gaetan.gilbert AT ens-lyon.fr>
Cc: coq-club AT inria.fr
Subject: Re: [Coq-Club] More than one ring structure (e.g. modulo ring) for one type
Date: Mon, 17 Jul 2017 14:18:40 +0200
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=e AT x80.org; spf=Pass smtp.mailfrom=e AT x80.org; spf=Pass smtp.helo=postmaster AT x80.org
Ironport-phdr: 9a23:bsuSQRXgn0aS37nvjrhG2lmbD8bV8LGtZVwlr6E/grcLSJyIuqrYYxGAt8tkgFKBZ4jH8fUM07OQ6PG/HzRYqb+681k6OKRWUBEEjchE1ycBO+WiTXPBEfjxciYhF95DXlI2t1uyMExSBdqsLwaK+i764jEdAAjwOhRoLerpBIHSk9631+ev8JHPfglEnjSwbLdwIRmssQndqtQdjJd/JKo21hbHuGZDdf5MxWNvK1KTnhL86dm18ZV+7SleuO8v+tBZX6nicKs2UbJXDDI9M2Ao/8LrrgXMTRGO5nQHTGoblAdDDhXf4xH7WpfxtTb6tvZ41SKHM8D6Uaw4VDK/5KpwVhTmlDkIOCI48GHPi8x/kqRboA66pxdix4LYeZyZOOZicq/Ye94RWGhPUdtLVyFZAo2ycZYBD+0PPehWrYbzpFUBohSiCgS3GOPj1iVFimPq0aAg0eksFxzN0gw6H9IJtXTZtMv6ObwdUO220KXE1zLDb+lZ2Tzg7ITGfRUhofCIXbJxdsra1E0hGB3ejk2KsozuIjKb2f4Js2if8eVgWuWvgHM7pgFrozig3NwshozPi4kIyV7E7T10zJs2KNC7UkJ3f8CoHZpKuy2HNYZ6X9kuT3xmtSok0rEKpJq2cSgQxJkkyRPTceGLf5WK7x75SuqcITh1iXR4c7ylnRmy61KvyujkW8m0zllKqi1Fn8HDt30OyxDf8M+HSuFy/ku52DaP0R7c6v1cLEwplqfWKIQtzqAumpcSq0jPAy37lFjsgKOLeEgo5PCk6+H9bbXnop+cOZV0igb7Mqk2hMOyGus5PwsSU2SB/uS8zrLj8VXjQLpWlv02jrXZsJfCKMsHoa65GhZZ3Zon6xaiFDiry88YnHkCLFJdYh2LlYnpO1fUIPD5F/izmVqskC04j8zBa5LoD4nEKDDskbPrcKxhoxpTwQcvxNYZ6JNQALwbPNr+XFS0sM3fCFk3KVrn7fzgDYBw/pNOASSIGKDRcI7XsFuJ4aoNLvIef8c6sTL5Jvcir9f0jHYi2AxONZK11IcaPSjrVs9tJF+UND+12o8M
Organization: X80 Heavy Industries

Gaetan Gilbert
<gaetan.gilbert AT ens-lyon.fr>
writes:

> You can also use a type alias.

Note that I don't know the inner working details of the ring tactic, but
the type alias approach could be problematic in a heavily automated
setting as Coq may unfold the alias at some point thus creating
problems.

E.

[Coq-Club] More than one ring structure (e.g. modulo ring) for one type, Soegtrop, Michael, 07/14/2017
- Re: [Coq-Club] More than one ring structure (e.g. modulo ring) for one type, Emilio Jesús Gallego Arias, 07/15/2017
  - RE: [Coq-Club] More than one ring structure (e.g. modulo ring) for one type, Soegtrop, Michael, 07/17/2017
    - Re: [Coq-Club] More than one ring structure (e.g. modulo ring) for one type, Emilio Jesús Gallego Arias, 07/17/2017
      - Re: [Coq-Club] More than one ring structure (e.g. modulo ring) for one type, Gaetan Gilbert, 07/17/2017
        
        RE: [Coq-Club] More than one ring structure (e.g. modulo ring) for one type, Soegtrop, Michael, 07/17/2017
        
        Re: [Coq-Club] More than one ring structure (e.g. modulo ring) for one type, Gaetan Gilbert, 07/17/2017
        
        RE: [Coq-Club] More than one ring structure (e.g. modulo ring) for one type, Soegtrop, Michael, 07/17/2017
        Re: [Coq-Club] More than one ring structure (e.g. modulo ring) for one type, Gaetan Gilbert, 07/17/2017
        
        Re: [Coq-Club] More than one ring structure (e.g. modulo ring) for one type, Emilio Jesús Gallego Arias, 07/17/2017