Command: Search - siegebell/vscoq GitHub Wiki

Search(list {constraintTypeN: string, constraintValueN: string, positiveConstraintN: boolean})

Searches for objects that satisfy a list of constraints. If positiveConstraint is false, then the constraint is inverted.

<call val="Search">
  <list>
    <pair>
      <search_cst val="${constraintType1}">
        ${constraintValue1}
      </search_cst>
      <bool val="${positiveConstraint1}"/>
    </pair>
    ...
    <!-- Example: -->
    <pair>
      <search_cst val="name_pattern">
        <string>bool_rect</string>
      </search_cst>
      <bool val="true"/>
    </pair>
  </list>
</call>

Returns

<value val="good">
  <list>
      <coq_object>
          <list>
              <string>${metaInfo}</string>
              ...
          </list>
          <list>
              <string>${name}</string>
          </list>
          <string>${definition}</string>
      </coq_object>
      ...
  </list>
</value>

Types of constraints:

  • Name pattern: constraintType = "name_pattern"; constraintValue is a regular expression string.
  • Type pattern: constraintType = "type_pattern"; constraintValue is a pattern (???: an open gallina term) string.
  • SubType pattern: constraintType = "subtype_pattern"; constraintValue is a pattern (???: an open gallina term) string.
  • In module: constraintType = "in_module"; constraintValue is a list of strings specifying the module/directory structure.
  • Include blacklist: constraintType = "include_blacklist"; constraintValue is ommitted.
Add a custom footer
⚠️ **GitHub.com Fallback** ⚠️