coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Confused about the "move" tactic

From: Wei Hu <weihu AT cs.virginia.edu>
To: coq-club AT pauillac.inria.fr
Subject: [Coq-Club] Confused about the "move" tactic
Date: Wed, 26 Sep 2007 13:48:45 -0400
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

Hi,

I had trouble understanding the behavior of "move".

For example, see this proof:

Goal forall a b c :Set, True.
intros.
move c after a.

The hypothesis c is now moved before a. But as I understand it, c should be
moved between a and b.
Why is that?

Thanks,
Wei

[Coq-Club] How to study "Calculus of Inductive Constructions", Wan Hai
- Re: [Coq-Club] How to study "Calculus of Inductive Constructions", Benjamin Pierce
- [Coq-Club] Confused about the "move" tactic, Wei Hu
  - Re: [Coq-Club] Confused about the "move" tactic, Hugo Herbelin