Skip to Content.
Sympa Menu

coq-club - [Coq-Club] guarantees from Print Assumptions

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] guarantees from Print Assumptions


Chronological Thread 
  • From: Abhishek Anand <abhishek.anand.iitg AT gmail.com>
  • To: coq-club <coq-club AT inria.fr>
  • Subject: [Coq-Club] guarantees from Print Assumptions
  • Date: Thu, 9 Jan 2014 15:09:32 -0500

Suppose I prove some theorem(say T) and then Print Assumptions T says:
"Closed under the global context".

Can I then be  sure that the proof does not (possibly indirectly) depend on some
unproved assumptions(Axioms, Admits)?

I'm not sure if I was dreaming, but I think that once Print Assumptions said that on a lemma
whose proof used other lemmas whose proofs had admits in them.
I can't replicate that problem today.


-- Abhishek
http://www.cs.cornell.edu/~aa755/



Archive powered by MHonArc 2.6.18.

Top of Page