coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Using Ssreflect in Coq

From: Théo Zimmermann <theo.zimmi AT gmail.com>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Using Ssreflect in Coq
Date: Wed, 5 Sep 2018 10:21:20 +0200
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=theo.zimmi AT gmail.com; spf=Pass smtp.mailfrom=theo.zimmi AT gmail.com; spf=None smtp.helo=postmaster AT mail-ua1-f53.google.com
Ironport-phdr: 9a23:b/fxbxCvPRCasad/sSymUyQJP3N1i/DPJgcQr6AfoPdwSPv4ocbcNUDSrc9gkEXOFd2Cra4c1KyO6+jJYi8p2d65qncMcZhBBVcuqP49uEgeOvODElDxN/XwbiY3T4xoXV5h+GynYwAOQJ6tL1LdrWev4jEMBx7xKRR6JvjvGo7Vks+7y/2+94fcbglUhjexe69+IAmrpgjNq8cahpdvJLwswRXTuHtIfOpWxWJsJV2Nmhv3+9m98p1+/SlOovwt78FPX7n0cKQ+VrxYES8pM3sp683xtBnMVhWA630BWWgLiBVIAgzF7BbnXpfttybxq+Rw1DWGMcDwULs5Xymp4aV2Rx/ykCoIODA5/2PXhMJ+j6xVvQyvqABkzoHOfI2YLuBzcr/Bcd4YQ2dKQ8ZfVzZGAoO5d4YBEeoBOvxfr4blpFQOrB6+BQyyC+P1zz9HnHn23asn2OkmDQHG3BIvH9UUvHXVrdX1MaISUeGuwanHyDXMdfJW2TPn5IfUdRAhpOiBULRtesTfzkkvEhnKjlSWqYH9PjOV0P4Ns2mB4OZ6W+KvkWgqoBxyrDi33soglJXFi4YPxl3H9Sh12pg5KcOmREJhYdOpHp1dvDyAOYRsWMMtWWRotT46yrIYvZ67ezAHyJE9yB7eb/yLapWI7Qj+WOqILzd1hHxodKiwhxa19kigxen8Wdeu3FlWqSpFl8HAtnEL1xPN9siKUuVx8lul1DqV1A3e6vtILV4qmabFMZIswrA9moIWsUvZHy/2nEv2jLWRdkUh4uWo9+TnbavhppOGNo50iwT+MqEvmsGkDuQ4NxIBX2mf+eimyLLj+kj5TK1QjvIqiqnZrIzaJcMDq6GlBA9Vy58v5Aq7Dze7y9sVhmIHLVJAeBKflYflIVDOIPbiDfe+mVugijlrx+qVdoHmV57KNz3IlKrrVbd78U9VjgQpnv5F4JcBNrGAJ8XBW0r0ucbdBxk/e1iow+vgTsd804YfcW2KC66ddqjVtAnbtaoUP+CQadpN637GIP8/6qu21C5rqRomZaCsmKAvRjW9F/ViLV+eZCO10NgEGGYO+AE5Sb6z0QHQYXtof3+3GpkEyHQjEov/VNXMQ4mshPqK2yLpRsQLNFADMUiFFDLTT6vBW/oIb3jPcMpokzhBSLH4DoF8jlehswj1z7chJe3RqHUV

Hello,

"From Coq Require Import ssreflect." is a one-line command to use SSReflect. The rest are just recommendations of the SSReflect authors that you are perfectly allowed to ignore.

You may also install the (still existing) coq-ssreflect package and do "From mathcomp Require Import ssreflect." in which case it will change these options for you (but also a few others).

Théo

Le mer. 5 sept. 2018 à 10:17, Frédéric Blanqui <frederic.blanqui AT inria.fr> a écrit :

Hello.

In https://coq.inria.fr/distrib/current/refman/proof-engine/ssreflect-proof-language.html?highlight=ssreflect#usage, it is written:

"All in all, this corresponds to working in the following context:

From Coq Require Import ssreflect ssrfun ssrbool.

Set Implicit Arguments.

Unset Strict Implicit.

Unset Printing Implicit Defensive."

Is this all we have to write before using Ssreflect? Isn't there a one-line command?

Frédéric.

[Coq-Club] Using Ssreflect in Coq, Frédéric Blanqui, 09/05/2018
- Re: [Coq-Club] Using Ssreflect in Coq, Théo Zimmermann, 09/05/2018
  - Re: [Coq-Club] Using Ssreflect in Coq, Frédéric Blanqui, 09/05/2018
  - Re: [Coq-Club] Using Ssreflect in Coq, Enrico Tassi, 09/05/2018