A rudimentary hash function on strings.

mk_hashed_name nspace id hashes the string id to a value i and returns the name nspace._i

copy_doc_string fr to copies the docstring from the declaration named fr to each declaration named in the list to.

copy_doc_string source → target_1 target_2 ... target_n copies the doc string of the declaration named source to each of target_1, target_2, ..., target_n.

A user attribute library_note for tagging decls of type string × string for use in note output.

mk_reflected_definition name val constructs a definition declaration by reflection.

Example: mk_reflected_definition `foo 17 constructs the definition declaration corresponding to def foo : ℕ := 17

If note_name and note are pexprs representing strings, add_library_note note_name note adds a declaration of type string × string and tags it with the library_note attribute.

A command to add library notes. Syntax:

/--
note message
-/
library_note "note id"

Collects all notes in the current environment. Returns a list of pairs (note_id, note_content)

Format a doc_category

format a tactic_doc_entry

update_description_from tde inh_id replaces the description field of tde with the doc string of the declaration named inh_id.

update_description tde replaces the description field of tde with:

• the doc string of tde.inherit_description_from, if this field has a value
• the doc string of the entry in tde.decl_names, if this field has length 1

If neither of these conditions are met, it returns tde.

A user attribute tactic_doc for tagging decls of type tactic_doc_entry for use in doc output

Collects everything in the environment tagged with the attribute tactic_doc.

add_tactic_doc tde adds a declaration to the environment with tde as its body and tags it with the tactic_doc attribute. If tde.decl_names has exactly one entry `decl and if tde.description is the empty string, add_tactic_doc uses the doc string of decl as the description.

A command used to add documentation for a tactic, command, hole command, or attribute.

Usage: after defining an interactive tactic, command, or attribute, add its documentation as follows.

/--
describe what the command does here
-/
add_tactic_doc
{ name := "display name of the tactic",
  category := cat,
  decl_names := [`dcl_1, `dcl_2],
  tags := ["tag_1", "tag_2"]
}

The argument to add_tactic_doc is a structure of type tactic_doc_entry.

• name refers to the display name of the tactic; it is used as the header of the doc entry.
• cat refers to the category of doc entry. Options: doc_category.tactic, doc_category.cmd, doc_category.hole_cmd, doc_category.attr
• decl_names is a list of the declarations associated with this doc. For instance, the entry for linarith would set decl_names := [`tactic.interactive.linarith]. Some entries may cover multiple declarations. It is only necessary to list the interactive versions of tactics.
• tags is an optional list of strings used to categorize entries.
• The doc string is the body of the entry. It can be formatted with markdown. What you are reading now is the description of add_tactic_doc.

If only one related declaration is listed in decl_names and if this invocation of add_tactic_doc does not have a doc string, the doc string of that declaration will become the body of the tactic doc entry. If there are multiple declarations, you can select the one to be used by passing a name to the inherit_description_from field.

If you prefer a tactic to have a doc string that is different then the doc entry, you should write the doc entry as a doc string for the add_tactic_doc invocation.

Note that providing a badly formed tactic_doc_entry to the command can result in strange error messages.

The add_decl_doc command is used to add a doc string to an existing declaration.

def foo := 5

/--
Doc string for foo.
-/
add_decl_doc foo