coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Ssreflect

From: Ranjani Krishnan <ranjani141 AT gmail.com>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Ssreflect
Date: Sun, 14 Feb 2016 09:12:53 +0530
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=ranjani141 AT gmail.com; spf=Pass smtp.mailfrom=ranjani141 AT gmail.com; spf=None smtp.helo=postmaster AT mail-ig0-f176.google.com
Ironport-phdr: 9a23:ZvhDdxf+kKRU0NnPJb1z1amglGMj4u6mDksu8pMizoh2WeGdxc6+Zh7h7PlgxGXEQZ/co6odzbGG7Oa7CSdauMbJmUtBWaIPfidNsd8RkQ0kDZzNImzAB9muURYHGt9fXkRu5XCxPBsdMs//Y1rPvi/6tmZKSV3BPAZ4bt74BpTVx5zukbvipNuIM04S3Wr1SIgxBSv1hD2ZjtMRj4pmJ/R54TryiVwMRd5rw3h1L0mYhRf265T41pdi9yNNp6BprJYYAu2pN5g/GLdfFXEtN30/zMztrxjKCwWVtVUGVWBDqBNOAQHD7VnZRJbqsi3zsKIpwiCcP8TwTOloAByt6q5qTFnjjyJRZG1xy33elsEl1PETmxmmvREqm4M=

I tried that too. With files that were getting compiled in Coq 8.4 also, it gets stuck at

"Running: coqc -I "E:\Code" "E:\Code\test.v" 2>&1" in 8.5

On Sat, Feb 13, 2016 at 3:34 PM, Laurent Thery <Laurent.Thery AT inria.fr> wrote:

On 02/13/2016 01:51 AM, Ranjani Krishnan wrote:

It's just 2 lines. I was trying out ssreflect :

Require Import Ssreflect.ssreflect Ssreflect.ssrfun Ssreflect.ssrbool
Ssreflect.eqtype Ssreflect.ssrnat Ssreflect.seq Ssreflect.tuple
Ssreflect.fintype.

Definition BITS n := n.-tuple bool.

If you are using 8.5

this should be

From mathcomp
Require Import ssreflect.ssrfun ssreflect.ssrbool ssreflect.eqtype ssreflect.ssrnat ssreflect.seq ssreflect.tuple ssreflect.fintype.

or simpler

From mathcomp Require Import all_ssreflect.

Thanks,

Ranjani

[Coq-Club] Ssreflect, Ranjani Krishnan, 02/09/2016
- Re: [Coq-Club] Ssreflect, Enrico Tassi, 02/09/2016
  - Re: [Coq-Club] Ssreflect, Ranjani Krishnan, 02/11/2016
    - Re: [Coq-Club] Ssreflect, Enrico Tassi, 02/11/2016
      - Re: [Coq-Club] Ssreflect, Ranjani Krishnan, 02/13/2016
        
        Re: [Coq-Club] Ssreflect, Laurent Thery, 02/13/2016
        
        Re: [Coq-Club] Ssreflect, Ranjani Krishnan, 02/14/2016