coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Laurent Théry <Laurent.Thery AT inria.fr>
- To: Arthur Azevedo de Amorim <arthur.aa AT gmail.com>, Coq Club <coq-club AT inria.fr>
- Subject: Re: [Coq-Club] [ssreflect] Ring, field and friends
- Date: Mon, 10 Aug 2015 12:26:04 +0200
On 09/08/15 05:08, Arthur Azevedo de Amorim wrote:
> Is there a way of using the standard Coq ring and field tactics with the
> structures in ssralg.v? In particular, can I get it to work with algC?
>
> Thanks
>
There is some unofficial code that let's
plug ssreflect and Loic Pottier's cring and nsatz tactics:
https://docs.google.com/document/d/1qRcQ5-UK5OusDz97m9nHGGyV-KnQh_af6GwMBjQO0Mw/edit?hl=fr
It seems still to work under 8.5 (with some modifications):
https://transfert.inria.fr/fichiers/6e844cd336d3fb11e50b56271fba683d/ssr_ncring.v
--
Laurent Théry
- Re: [Coq-Club] [ssreflect] Ring, field and friends, Laurent Théry, 08/10/2015
- <Possible follow-up(s)>
- Re: [Coq-Club] [ssreflect] Ring, field and friends, Laurent Théry, 08/10/2015
Archive powered by MHonArc 2.6.18.