coq-club AT inria.fr

Subject: The Coq mailing list

List archive

Re: [Coq-Club] Simple question about tactic notation

From: "Samuel E. Moelius III" <moelius AT cis.udel.edu>
To: Edsko de Vries <devriese AT cs.tcd.ie>
Cc: coq-club AT pauillac.inria.fr
Subject: Re: [Coq-Club] Simple question about tactic notation
Date: Sun, 15 Mar 2009 12:56:58 -0400
List-archive: <http://pauillac.inria.fr/pipermail/coq-club/>

If you change ``integer'' to ``constr'' in the definition of my_induction, then you no longer get the error.

(*=======================================================================*)

Tactic Notation "my_induction" constr(n) :=
  induction n.

Inductive even : nat -> Prop :=
  | even_zero : even 0
  | even_succ : forall n, even n -> even (S (S n)).

Lemma foo : forall (n:nat), even n -> True.
Proof.
  my_induction 1; tauto.
Qed.

(*=======================================================================*)

Sam

[Coq-Club] Simple question about tactic notation, Edsko de Vries
- Re: [Coq-Club] Simple question about tactic notation, Thomas Braibant
  - Re: [Coq-Club] Simple question about tactic notation, Samuel E. Moelius III
    - Re: [Coq-Club] Simple question about tactic notation, Edsko de Vries
      - Re: [Coq-Club] Simple question about tactic notation, Samuel E. Moelius III
        
        Re: [Coq-Club] Simple question about tactic notation, Samuel E. Moelius III
        
        Re: [Coq-Club] Simple question about tactic notation, Edsko de Vries
  - Re: [Coq-Club] Simple question about tactic notation, Edsko de Vries
    - Re: [Coq-Club] Simple question about tactic notation, Edsko de Vries
- Re: [Coq-Club] Simple question about tactic notation, Hugo Herbelin