coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Ssreflect

From: Laurent Thery <Laurent.Thery AT inria.fr>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Ssreflect
Date: Sat, 13 Feb 2016 11:04:55 +0100

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.

[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