coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Trouble constructing terms of dependent types involving proofs

From: Ralf Jung <jung AT mpi-sws.org>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Trouble constructing terms of dependent types involving proofs
Date: Thu, 3 Mar 2016 21:58:01 +0100
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=jung AT mpi-sws.org; spf=Pass smtp.mailfrom=jung AT mpi-sws.org; spf=None smtp.helo=postmaster AT hera.mpi-klsb.mpg.de
Ironport-phdr: 9a23:SlIRVBHeGmERoMKTmQs0p51GYnF86YWxBRYc798ds5kLTJ75pM2wAkXT6L1XgUPTWs2DsrQf27WQ7PyrADdRqb+681k8M7V0HycfjssXmwFySOWkMmbcaMDQUiohAc5ZX0Vk9XzoeWJcGcL5ekGA6ibqtW1aJBzzOEJPK/jvHcaK1oLsh7/0pMGYOl4ZzBOGIppMbzyO5T3LsccXhYYwYo0Q8TDu5kVyRuJN2GlzLkiSlRuvru25/Zpk7jgC86l5r50IAu3GePEzSqUdBzA7OUg04tfqvF/NV1ih/HwZB18flhQAIRXD41muXIr3vQP/rus4wzaBe8rsQuZnCnyZ8653RUqw2288PDkj/TSPhw==

Hi again,

I got the suggestion to install unicoq, so I did. This changes the
error, but test2 still fails:

> Error: The term "eq_refl" has type "?x = ?x" while it is expected to have
> type "in_dec_bool "x" ?l0 = true".

Kind regards,
Ralf

[Coq-Club] Trouble constructing terms of dependent types involving proofs, Ralf Jung, 03/03/2016
- Re: [Coq-Club] Trouble constructing terms of dependent types involving proofs, Jonathan Leivent, 03/03/2016
  - Re: [Coq-Club] Trouble constructing terms of dependent types involving proofs, Ralf Jung, 03/03/2016
    - Re: [Coq-Club] Trouble constructing terms of dependent types involving proofs, Clément Pit--Claudel, 03/03/2016
      - Re: [Coq-Club] Trouble constructing terms of dependent types involving proofs, Ralf Jung, 03/03/2016
        
        Re: [Coq-Club] Trouble constructing terms of dependent types involving proofs, Clément Pit--Claudel, 03/03/2016
        
        Re: [Coq-Club] Trouble constructing terms of dependent types involving proofs, Clément Pit--Claudel, 03/03/2016
- Re: [Coq-Club] Trouble constructing terms of dependent types involving proofs, Ralf Jung, 03/03/2016
- Re: [Coq-Club] Trouble constructing terms of dependent types involving proofs, Robbert Krebbers, 03/03/2016
  - Re: [Coq-Club] Trouble constructing terms of dependent types involving proofs, Robbert Krebbers, 03/03/2016
    - Re: [Coq-Club] Trouble constructing terms of dependent types involving proofs, Clément Pit--Claudel, 03/03/2016
      - Re: [Coq-Club] Trouble constructing terms of dependent types involving proofs, Ralf Jung, 03/04/2016
        
        Re: [Coq-Club] Trouble constructing terms of dependent types involving proofs, Gregory Malecha, 03/05/2016
        
        Re: [Coq-Club] Trouble constructing terms of dependent types involving proofs, Ralf Jung, 03/06/2016
        
        Re: [Coq-Club] Trouble constructing terms of dependent types involving proofs, Jonathan Leivent, 03/06/2016
        Re: [Coq-Club] Trouble constructing terms of dependent types involving proofs, Gregory Malecha, 03/07/2016