matchp

DB.matchp : (thm -> bool) -> string list -> data list

All theory elements satisfying a predicate.

An invocation matchp P [thy1,...,thyn] collects all elements of the theory segments thy1,…,thyn that P holds of. If the list of theory segments is empty, then all currently loaded segments are examined. The string "-" may be used to designate the current theory segment.

Failure

Fails if P fails when applied to a theorem in one of the theories being searched.

Example

The following query returns all unconditional rewrite rules in the theory pair.

> matchp (is_eq o snd o strip_forall o concl) ["pair"];
val it =
   [(("pair", "C_UNCURRY_L"),
     (⊢ flip (UNCURRY f) x = UNCURRY (flip (flip ∘ f) x), Thm,
      Located
       {exact = true, linenum = 602, scriptpath =
        "$(HOLDIR)/src/coretypes/pairScript.sml"})),
    (("pair", "CLOSED_PAIR_EQ"),
     (⊢ ∀x y a b. (x,y) = (a,b) ⇔ x = a ∧ y = b, Thm,
      Located
       {exact = true, linenum = 106, scriptpath =
        "$(HOLDIR)/src/coretypes/pairScript.sml"})),
    (("pair", "COMMA_DEF"),
     (⊢ ∀x y. (x,y) = ABS_prod (λa b. a = x ∧ b = y), Def, Unknown)),
    (("pair", "CURRY_DEF"), (⊢ ∀f x y. CURRY f x y = f (x,y), Def, Unknown)),
    (("pair", "CURRY_DEF_lazyfied"),
[...Output elided...]

See also

DB.match, DB.matcher, DB.apropos, DB.find