coq-club AT inria.fr

Subject: The Coq mailing list

List archive

From: Jonathan Leivent <jonikelee AT gmail.com>
To: Coq Club <coq-club AT inria.fr>
Subject: [Coq-Club] decide equality on more types
Date: Mon, 4 Jul 2016 18:55:03 -0400
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=jonikelee AT gmail.com; spf=Pass smtp.mailfrom=jonikelee AT gmail.com; spf=None smtp.helo=postmaster AT mail-qk0-f169.google.com
Ironport-phdr: 9a23:U26IWxaLNx62S9VoYA2SxDP/LSx+4OfEezUN459isYplN5qZpcq8bnLW6fgltlLVR4KTs6sC0LuO9fq7EjZZqb+681k6OKRWUBEEjchE1ycBO+WiTXPBEfjxciYhF95DXlI2t1uyMExSBdqsLwaK+i760zceF13FOBZvIaytQ8iJ3pzxjbv5ocSbSj4LrQL1Wal1IhSyoFeZnegtqqwmFJwMzADUqGBDYeVcyDAgD1uSmxHh+pX4p8Y7oGx48sgs/M9YUKj8Y79wDfkBVGxnYCgJ45jAsgCLZg+S7DNIWWIP1xFMHgLt7RfgX563vDGs5cRn3yzPH8rwRKw0UDLqy6pqVhLulG9TNTk/8WLajsF9pK1eqROl4Rd4xtiHM8muKPNic/aFLpshTm1bU5MUDnQZDw==

Does anyone know of a version of the "decide equality" tactic that works on more types?

-- Jonathan

[Coq-Club] decide equality on more types, Jonathan Leivent, 07/05/2016
- Re: [Coq-Club] decide equality on more types, Jason Gross, 07/05/2016
  - Re: [Coq-Club] decide equality on more types, Jonathan Leivent, 07/05/2016
    - Re: [Coq-Club] decide equality on more types, Jason Gross, 07/05/2016
      - Re: [Coq-Club] decide equality on more types, Jonathan Leivent, 07/06/2016
        
        [Coq-Club] Ltac way to detect symbol definedness (was Re: decide equality on more types), Jonathan Leivent, 07/06/2016
        
        Re: [Coq-Club] decide equality on more types, Matthieu Sozeau, 07/08/2016
        
        Re: [Coq-Club] decide equality on more types, Jonathan Leivent, 07/08/2016
        
        Re: [Coq-Club] decide equality on more types, Jonathan Leivent, 07/08/2016
        Re: [Coq-Club] decide equality on more types, Jonathan Leivent, 07/08/2016