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: Sat, 13 Feb 2016 06:21:22 +0530
Authentication-results: mail3-smtp-sop.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-io0-f181.google.com
Ironport-phdr: 9a23:BKieiRY798GewpQWts5zqUP/LSx+4OfEezUN459isYplN5qZpci6bnLW6fgltlLVR4KTs6sC0LqJ9fu/Ejdcqb+681k8M7V0HycfjssXmwFySOWkMmbcaMDQUiohAc5ZX0Vk9XzoeWJcGcL5ekGA6ibqtW1aJBzzOEJPK/jvHcaK1oLsh7/0oMKYOFkArQH+SI0xBS3+lR/WuMgSjNkqAYcK4TyNnEF1ff9Lz3hjP1OZkkW0zM6x+Jl+73YY4Kp5pIYTGZn9Kq8/VPlTCCksG2Ez/szi8xfZHiWV4X5JaGwQkBNOAkDm9hDhXpH4tGOurON72iCcPJSqFJg7XD2j6+FgTxq+23RPDCIw7GyC0p84t6lcuh/0/xE=

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.

On Thu, Feb 11, 2016 at 1:29 PM, Enrico Tassi <enrico.tassi AT inria.fr> wrote:

On Thu, Feb 11, 2016 at 07:31:57AM +0530, Ranjani Krishnan wrote:
> Thank you. I installed coq 8.5. But when I try to compile my file, it gets
> stuck at 'running..'
> How do I know if the compilation was successful?

Hum, I can't really help you without having your file at hand. Can you
share it?

Best,
--
Enrico Tassi

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