Skip to Content.
Sympa Menu

coq-club - [Coq-Club] Pattern matching on hypotheses of certain types

coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Pattern matching on hypotheses of certain types


Chronological Thread 
  • From: Jason Gross <jasongross9 AT gmail.com>
  • To: coq-club <coq-club AT inria.fr>
  • Subject: [Coq-Club] Pattern matching on hypotheses of certain types
  • Date: Thu, 9 Aug 2012 03:48:11 -0400

Hi,
Is there a good way to get [match goal with ... end] to respect the typing/naming of hypotheses?  That is, is there a variant of
    Goal forall (n m : nat) (n' m' : unit) (f : nat -> nat -> Type) (f' : unit -> unit -> Type) (P : nat -> Prop) (fn : P n -> f n m -> f' n' m'), False.
      intros.
      match goal with
        | [ H : unit -> unit -> _, H1 : appcontext[?H ?a ?b] |- _ ] => pose H
      end.
that gives me a new hypothesis [T := f' : unit -> unit -> Type] rather than [T := f : nat -> nat -> Type]?  (I know that I can match for the type of [H] after the fact, but this seems like it gets unwieldy quickly, if I have multiple hypotheses that I'm trying to match against simultaneously.)

Thanks.

-Jason



Archive powered by MHonArc 2.6.18.

Top of Page