The Coq mailing list

[Anthony Canino <anthony.canino1 AT gmail.com>]

Hi all,

I'm working through Software Foundations, and the following notation is introduced for the typing relation for the simply typed lambda calculus

Reserved Notation "Gamma '|-' t '\in' T" (at level 40).

This makes sense, but when trying to automate a proof, I think I am running into a conflict using |-.

match goal with
  | [ H : forall T, ?H1 -> forall x, ?H2 -> False |- _ ]  => eapply H; eassumption
end.

Toplevel input, characters 73-74:
Syntax error: '\in' expected after [constr:operconstr level 200] (in [constr:operconstr]).

The error makes perfect sense to me; Coq is looking for the \in from the notation introduction. My question is, since |- is used for matching goals, is there a clean way to also use |- for custom notations?

Thanks,

Anthony

 

--

Anthony