From f0376c08b6deca172122410674c252e18099413e Mon Sep 17 00:00:00 2001 From: Pierre Rousselin Date: Sat, 27 Apr 2024 20:12:15 +0200 Subject: [PATCH] Update refman's Search documentation --- doc/sphinx/proof-engine/vernacular-commands.rst | 9 ++++++++- 1 file changed, 8 insertions(+), 1 deletion(-) diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst index 63b4a874a8f1e..12c2ce92fb18d 100644 --- a/doc/sphinx/proof-engine/vernacular-commands.rst +++ b/doc/sphinx/proof-engine/vernacular-commands.rst @@ -198,7 +198,7 @@ described elsewhere Filters objects by the keyword that was used to define them (`Theorem`, `Lemma`, `Axiom`, `Variable`, `Context`, `Primitive`...) or its status (`Coercion`, `Instance`, `Scheme`, - `Canonical`, `SubClass`, Field` for record fields, `Method` for class + `Canonical`, `SubClass`, `Field` for record fields, `Method` for class fields). Note that `Coercion`\s, `Canonical Structure`\s, Instance`\s and `Scheme`\s can be defined without using those keywords. See :ref:`this example `. @@ -308,6 +308,13 @@ described elsewhere Search is:Instance [ Reflexive | Symmetric ]. + The following search outputs operations on `nat` defined in the + prelude either with the `Definition` or `Fixpoint` keyword: + + .. coqtop:: all reset + + Search (nat -> nat -> nat) -bool [ is:Definition | is:Fixpoint ]. + .. cmd:: SearchPattern @one_pattern {? {| inside | in | outside } {+ @qualid } } Displays the name and type of all hypotheses of the