mathlib documentation

tactic.doc_commands

Documentation commands #

We generate html documentation from mathlib. It is convenient to collect lists of tactics, commands, notes, etc. To facilitate this, we declare these documentation entries in the library using special commands.

Since these commands are used in files imported by tactic.core, this file has no imports.

Implementation details #

library_note note_id note_msg creates a declaration `library_note.i for some i. This declaration is a pair of strings note_id and note_msg, and it gets tagged with the library_note attribute.

Similarly, add_tactic_doc creates a declaration `tactic_doc.i that stores the provided information.

def string.hash (s : string) :

A rudimentary hash function on strings.

Equations
meta def string.mk_hashed_name (nspace : name) (id : string) :

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

meta def tactic.copy_doc_string (fr : name) (to : list name) :

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

meta def copy_doc_string_cmd (_x : interactive.parse (lean.parser.tk "copy_doc_string")) :

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.

The library_note command #

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

meta def mk_reflected_definition (decl_name : name) {type : Sort u_1} [reflected type] (body : type) [reflected body] :

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

meta def tactic.add_library_note (note_name note : string) :

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)

The add_tactic_doc_entry command #

inductive doc_category  :
Type

The categories of tactic doc entry.

@[protected, instance]
@[protected, instance]
@[protected, instance]
structure tactic_doc_entry  :
Type

The information used to generate a tactic doc entry

Turns a tactic_doc_entry into a JSON representation.

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
```