Ssreflect Users Discussion List

[Laurent Thery <>]

On 02/22/2016 07:39 PM, Guillaume Melquiond wrote:
> On 22/02/2016 17:56, Ralf Jung wrote:
> > >Hi,
> > >
> > > >>Have you ever wanted to rewrite using wildcards not only on the
> > > >>left-hand side but also on the right-hand side of an equality? Are you
> > > >>using Coq 8.5? Then the following trick might be of help to you:
> > > >>
> > > >>Lemma foo x y : x + 3 + y = 3 + x + y.
> > > >>rewrite (_ : ?[n] + 3 = 3 + ?n).
> > >
> > >Consider me confused. Is this "?[n]" business a feature available for
> > >all pattern matching, e.g. also for "rewrite [?[n] + n]lemma" to find an
> > >application of plus with twice the same argument?
> Hopefully yes.

I don't know if it is intended but this seems not to work with Search:

From mathcomp Require Import all_ssreflect.

Axiom bar : forall x : nat, x + x = 0.
Axiom bar1 : forall x y : nat, x + y = 0.

Search _ (?[n] + ?n) "bar".

returns
 bar and bar1

--
Laurent