coq-club AT inria.fr
Subject: The Coq mailing list
List archive
- From: Keiko Nakata <keiko AT kurims.kyoto-u.ac.jp>
- To: coq-club AT pauillac.inria.fr
- Subject: [Coq-Club] Can Qed raise a type error?
- Date: Wed, 09 Jul 2008 17:13:15 +0900 (JST)
- List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>
Hello.
Is it possible that "Qed" ends up with a type error,
or other serious errors except for the out of memory?
I never omit to instantiate existential variables,
no metavariables are left (e.g. no eauto or eapply),
or I do not use co-induction.
Currently I do not want to struggle with the out of memory problem
which I incur by Qed, but I want to be sure my proof term is correct.
With best regards,
Keiko
- [Coq-Club] Can Qed raise a type error?, Keiko Nakata
- Re: [Coq-Club] Can Qed raise a type error?,
vsiles
- Re: [Coq-Club] Can Qed raise a type error?,
Keiko Nakata
- Re: [Coq-Club] Can Qed raise a type error?,
Julien Forest
- [Coq-Club] Naming a term vs. using the term directly., Razvan Voicu
- Re: [Coq-Club] Can Qed raise a type error?, Xavier Leroy
- Message not available
- Re: [Coq-Club] Can Qed raise a type error?, Keiko Nakata
- Re: [Coq-Club] Can Qed raise a type error?,
Julien Forest
- Re: [Coq-Club] Can Qed raise a type error?,
Keiko Nakata
- Re: [Coq-Club] Can Qed raise a type error?,
vsiles
Archive powered by MhonArc 2.6.16.