coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [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: Re: [Coq-Club] Can Qed raise a type error?
Date: Wed, 09 Jul 2008 17:33:54 +0900 (JST)
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

> by using the tactic "fix" without being cautious, you can complete a proof
> but the Qed failed, mostly because your recursive call was not on a sub
> term.
>
> That's the only case I know where Qed can failed.

Thank you for the informative advice.
Fortunately I am not using "fix", so your reply sounds a good news to me.

Best,
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