Skip to Content.
Sympa Menu

coq-club - [Coq-Club] Can Qed raise a type error?

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Can Qed raise a type error?


chronological Thread 
  • 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





Archive powered by MhonArc 2.6.16.

Top of Page