Skip to Content.
Sympa Menu

coq-club - Re: [Coq-Club] calculating values depending on the structure of proofs

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] calculating values depending on the structure of proofs


chronological Thread 
  • From: CHA Reeseo <reeseo AT formal.korea.ac.kr>
  • To: coq-club <coq-club AT inria.fr>
  • Subject: Re: [Coq-Club] calculating values depending on the structure of proofs
  • Date: Thu, 8 Apr 2010 07:32:35 +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 :content-transfer-encoding; b=aO7PRaWD7HNmSNGy5e3f+MDFuvWMzsxrKL+kjTBfDYxN/GpaqPHQMy93zL80mu4eRK GNllzzYYCajlAeJmToVUIvU2wAD1Lzr24ODhw7yMUc6NSdG8eFju4SbKZW6XhQ9b8y3N 6pNHmntgKy/mSNQ5/TfkgqmEgsctwvs6/vZkU=
2010/4/8 Adam Chlipala 
<adam AT chlipala.net>:
> That's an interesting idea.  The command [Show Existentials] will print the
> contexts of all remaining existential variables, which at least conveys all
> the same information, though in a more verbose form.

2010/4/8 Matthieu Sozeau 
<mattam AT mattam.org>:
> Le 7 avr. 2010 à 18:08, Adam Koprowski a écrit :
>>   I believe that 'Show Existentials' is what you are looking for: 
>> http://coq.inria.fr/refman/Reference-Manual010.html#@command192.
>
> The command [Set Printing Existential Instances] might be useful too,
> it prints the substitution applied to the existential.

Thank you all.  All of them are very useful.  :^)

-- 
CHA Reeseo
http://www.reeseo.net/


Archive powered by MhonArc 2.6.16.

Top of Page