Ssreflect Users Discussion List

[Georges Gonthier <>]

 Indeed; Search _ perm_eq in seq.
also works the same, and is one character shorter. Also note that results 
about perm_eq are often stated using the perm_eql predicate, so you might 
want to search that instead.

  Cheers,
Georges

-----Original Message-----
From: Laurent Théry [] 
Sent: 27 April 2010 09:35
To: Sean McLaughlin
Cc: 
Subject: Re: Search problem

Sean McLaughlin wrote:
> Hi,
>
>   I'm having trouble using the Search command.  For instance:
>
> Require Import ssreflect ssrbool ssrfun eqtype ssrnat fintype finset seq.
>
> Search perm_eq in seq.
>
> produces
>
> perm_eq_refl  forall (T : eqType) (s : seq T), perm_eq (T:=T) s s
> uniq_perm_eq
>    forall (T : eqType) (s1 s2 : seq T),
>    uniq s1 -> uniq s2 -> s1 =i s2 -> perm_eq (T:=T) s1 s2
>
> while there are many more theorems involving perm_eq.  What am I doing 
> wrong?
>

Hi,

Search perm_eq in seq.

is matching only the theorems conclusion with perm_eq, if you want also 
theorem with assumption
that contains perm_eq.


Search "" perm_eq in seq.

--
Laurent