From 9e677bc566a57a45f4e7604126c42ae97490ab8f 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 | 11 +++++++++-- 1 file changed, 9 insertions(+), 2 deletions(-) diff --git a/doc/sphinx/proof-engine/vernacular-commands.rst b/doc/sphinx/proof-engine/vernacular-commands.rst index 63b4a874a8f1..962deff27e5f 100644 --- a/doc/sphinx/proof-engine/vernacular-commands.rst +++ b/doc/sphinx/proof-engine/vernacular-commands.rst @@ -198,8 +198,8 @@ 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 - fields). Note that `Coercion`\s, `Canonical Structure`\s, Instance`\s and `Scheme`\s can be + `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 `. Additional clauses: @@ -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