coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: CHA Reeseo <reeseo AT formal.korea.ac.kr>
- To: coq-club <coq-club AT inria.fr>
- Subject: [Coq-Club] Re: calculating values depending on the structure of proofs
- Date: Thu, 8 Apr 2010 04:11:58 +0900
- Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:sender:in-reply-to:references:date :x-google-sender-auth:message-id:subject:from:to:content-type; b=wiFOZZznEyaJ7s2O0Ct6BQWdN2QvMK++iYSbY1hqNbfSRnW4HFlawWGT+YdF0Sq/d6 gjcKX+9Sqp0umOD72BDlbzkk0rLhA35ej0I8r6sEZpy8XQozL/8oG2RSjRMszZe1C02p DUu3GPblqwZDi+c+LbGvfIU5j/LR4Z6V+sVmo=
2010/4/8 CHA Reeseo
<reeseo AT formal.korea.ac.kr>:
> QUESTION 1: Is there really no way to retrieve detailed information from
> the proofs of inductive predicates (whose final type is Prop) when the
> current goal has sort Set?
An amplification: If there is any way to do this, I don't care even if I
cannot generate source code in Haskell or Ocaml from the Coq function
defined (proved) in that way.
--
CHA Reeseo
http://www.reeseo.net/
- [Coq-Club] calculating values depending on the structure of proofs, CHA Reeseo
- [Coq-Club] Re: calculating values depending on the structure of proofs, CHA Reeseo
- Re: [Coq-Club] calculating values depending on the structure of proofs, Adam Chlipala
- Re: [Coq-Club] calculating values depending on the structure of proofs, Jean-Francois Monin
Archive powered by MhonArc 2.6.16.