Ssreflect Users Discussion List

[Laurent Théry <>]

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