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.

library_note adds a note describing a certain feature or design decision. These can be referenced in doc strings with the text note [name of note].
add_tactic_doc adds an entry documenting an interactive tactic, command, hole command, or attribute.

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

s.hash = string.fold 1 (λ (h : ℕ) (c : char), (33 * h + c.val) % unsigned_sz) s

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")) :

lean.parser unit

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 #

meta def library_note_attr :

(user_attribute unit)

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.

meta def library_note (mi : interactive.decl_meta_info) (_x : interactive.parse (lean.parser.tk "library_note")) :

lean.parser unit

A command to add library notes. Syntax:

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

meta def tactic.get_library_notes :

tactic (list (string × string))

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

tactic : doc_category
cmd : doc_category
hole_cmd : doc_category
attr : doc_category

The categories of tactic doc entry.

@[protected, instance]

def doc_category.decidable_eq :

decidable_eq doc_category

@[protected, instance]

meta def doc_category.has_reflect :

has_reflect doc_category

meta def doc_category.to_string :

doc_category → string

Format a doc_category

@[protected, instance]

meta def doc_category.has_to_format :

has_to_format doc_category

@[protected, instance]

meta def tactic_doc_entry.has_reflect :

has_reflect tactic_doc_entry

structure tactic_doc_entry :

Type

name : string
category : doc_category
decl_names : list name
tags : list string
description : string
inherit_description_from : option name

The information used to generate a tactic doc entry

meta def tactic_doc_entry.to_json (d : tactic_doc_entry) :

Turns a tactic_doc_entry into a JSON representation.

@[protected, instance]

meta def tactic_doc_entry.has_to_string :

has_to_string tactic_doc_entry

meta def tactic_doc_entry.update_description_from (tde : tactic_doc_entry) (inh_id : name) :

tactic 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.

meta def tactic_doc_entry.update_description (tde : tactic_doc_entry) :

tactic tactic_doc_entry

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.

meta def tactic_doc_entry_attr :

(user_attribute unit)

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

meta def tactic.get_tactic_doc_entries :

tactic (list tactic_doc_entry)

Collects everything in the environment tagged with the attribute tactic_doc.

meta def tactic.add_tactic_doc (tde : tactic_doc_entry) :

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.

meta def add_tactic_doc_command (mi : interactive.decl_meta_info) (_x : interactive.parse (lean.parser.tk "add_tactic_doc")) :

lean.parser unit

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.

meta def add_decl_doc_command (mi : interactive.decl_meta_info) (_x : interactive.parse (lean.parser.tk "add_decl_doc")) :

lean.parser unit

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