The Coq mailing list

[Abhishek Kr Singh <abhishek.uor AT gmail.com>]

Hi,

I have the following definition for an  ordType and infix notations for its boolean comparison operators ==, <b and <=b

Module Order. Structure type: Type:= Pack { sort: Type; eqb: sort-> sort -> bool; ltb: sort-> sort -> bool; eq_P: forall x y, reflect (eq x y)(eqb x y); ltb_irefl: forall x, ltb x x=false; ltb_antisym: forall x y, x<>y -> ltb x y = negb (ltb y x); ltb_trans: forall x y z, ltb x y -> ltb y z -> ltb x z }. Module Exports. Coercion sort : type >-> Sortclass. Notation ordType:= type. End Exports. End Order. Export Order.Exports.

Definition sort:= Order.sort. Definition eqb := Order.eqb. Definition ltb := Order.ltb.


Notation "x == y":= (@eqb _ x y)(at level 50, no associativity): bool_scope. Notation "x <b y":= (@ltb _ x y)(at level 0, no associativity): bool_scope. Notation " x <=b y" := (@leb _ x y)(at level 70, no associativity): bool_scope.


Now consider the following Ltac definition for show_H which should print the hypothesis whose type is of the form x == y.

 Ltac show_H:=
    match goal with
    | H: ?x == ?y |- _ =>  idtac H
    end.

However, when I use this definition to show the name of hypothesis in the following Lemma it fails with the following error message.

Lemma triv (T:ordType)(x y:T): x == y -> y <b x -> 2=3.
Proof. intros. show_H.

(Error: No matching clauses for match.)

Why is the parser unable to match the notation == in the hypothesis ?

--

Thanks and Regards.

Abhishek Kr. Singh,
Research Scholar, STCS, TIFR Mumbai.
Homepage:  http://www.tcs.tifr.res.in/~abhishek/

 http://www.tcs.tifr.res.in/people/abhishek-singh