mathcomp/ssrtest/explain_match.v


1
2
3
4
5
6
7
8
9
10
11
12

Require Import ssreflect ssrbool ssrnat.

Definition addnAC := (addnA, addnC).

Lemma test x y z : x + y + z =  x + y.

ssrinstancesoftpat (_ + _).
ssrinstancesofruleL2R addnC.
ssrinstancesofruleR2L addnA.
ssrinstancesofruleR2L addnAC.
Fail ssrinstancesoftpat (_ + _ in RHS). (* Not implemented *)
Admitted.