coq-club AT inria.fr

Subject: The Coq mailing list

List archive

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

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