coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- 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/- [Coq-Club] guarantees from Print Assumptions, Abhishek Anand, 01/09/2014
- Re: [Coq-Club] guarantees from Print Assumptions, Arnaud Spiwack, 01/10/2014
- Re: [Coq-Club] guarantees from Print Assumptions, Abhishek Anand, 01/14/2014
- Re: [Coq-Club] guarantees from Print Assumptions, Arnaud Spiwack, 01/10/2014
Archive powered by MHonArc 2.6.18.