ssreflect - Search problem

Subject: Ssreflect Users Discussion List

List archive

From: Sean McLaughlin <>
To:
Subject: Search problem
Date: Wed, 21 Apr 2010 15:43:59 -0700
Domainkey-signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:from:date:message-id:subject:to:content-type; b=DKOw3hbe5cVt8zesXNSrtqbF4rP84/zpKpFfRzcLwToqfq3S/nnO6WTPaLZ0nAK7DK NkymwiBJnJ746F0OxSH82faI911e0bAOG25Gp4b1mnQCsYL4Q4Fb2fGT0rzZlK22dAHB 6K8mVWEWc0DLTg8fYp0KHNx2K2BV/hg8yf1AU=

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?

Sean

Search problem, Sean McLaughlin, 04/22/2010
- Re: Search problem, Laurent Théry, 04/27/2010
  - RE: Search problem, Georges Gonthier, 04/27/2010