coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

From: Clément Pit--Claudel <clement.pit AT gmail.com>
To: coq-club AT inria.fr
Subject: Re: [Coq-Club] Trouble constructing terms of dependent types involving proofs
Date: Thu, 3 Mar 2016 14:20:29 -0700
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=clement.pit AT gmail.com; spf=SoftFail smtp.mailfrom=clement.pit AT gmail.com; spf=None smtp.helo=postmaster AT mout.kundenserver.de
Ironport-phdr: 9a23:vXQK3BOs/Szn4uXScVol6mtUPXoX/o7sNwtQ0KIMzox0KPj8rarrMEGX3/hxlliBBdydsKIbzbWK+Pm7CCQp2tWojjMrSNR0TRgLiMEbzUQLIfWuLgnFFsPsdDEwB89YVVVorDmROElRH9viNRWJ+iXhpQAbFhi3DwdpPOO9QteU1JTokb/usMSIMk1hv3mUX/BbFF2OtwLft80b08NJC50a7V/3mEZOYPlc3mhyJFiezF7W78a0+4N/oWwL46pyv50IbaKvdKMhCLdcET4OMmYv5cStuwOQYxGI4y43VuQTnxxUNDDE8FS/dZP4ryf3sqIp0y2XOMDwUfYsWCiK4KJiSRuugyACYW1quFrLg9B92foI6CmqoAZyltbZ

On 03/03/2016 02:03 PM, Ralf Jung wrote:
> Lemma lem1 ... :
> HoareTriple ... (Lam _ "x" (...)) ...

Are you running 8.5? Maybe Jonathan can provide a fancy example of
tactics-in-terms? :)

Clément.

Attachment: signature.asc
Description: OpenPGP digital signature

[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