mathlib documentation

<unknown> / src.export_json

Used to generate a json file for html docs.

The json file is a list of maps, where each map has the structure

interface DeclInfo {
  name: string;
  args: efmt[];
  type: efmt;
  doc_string: string;
  filename: string;
  line: int;
  attributes: string[];
  equations: efmt[];
  kind: string;
  structure_fields: [string, efmt][];
  constructors: [string, efmt][];
}

Where efmt is defined as follows ('c' is a concatenation, 'n' is nesting):

type efmt = ['c', efmt, efmt] | ['n', efmt] | string;

Include this file somewhere in mathlib, e.g. in the scripts directory. Make sure mathlib is precompiled, with all.lean generated by mk_all.sh.

Usage: lean entrypoint.lean prints the generated JSON to stdout. entrypoint.lean imports this file.

source
meta def string.is_whitespace (s : string) :
bool
source
meta def string.has_whitespace (s : string) :
bool
source
meta def json.of_string_list (xs : list string) :
json
source
meta inductive efmt  :
Type
source
@[protected, instance]
meta def efmt.has_append  :
has_append efmt
source
@[protected, instance]
meta def efmt.has_coe  :
has_coe string efmt
source
@[protected, instance]
meta def efmt.coe_format  :
has_coe format efmt
source
meta def efmt.to_json  :
efmt → json
source
meta def efmt.compose'  :
efmt → efmt → efmt
source
meta def efmt.of_eformat  :
eformat → efmt
source
meta def efmt.sink_lparens_core  :
list string → efmt → efmt
source
meta def efmt.sink_rparens_core  :
efmt → list string → efmt
source
meta def efmt.sink_parens (e : efmt) :
efmt
source
meta def efmt.simplify  :
efmt → efmt
source
meta def efmt.pp (e : expr) :
tactic efmt
source
meta def expr.instantiate_pis  :
list expr → expr → expr
source
meta structure decl_info  :
Type

The information collected from each declaration

source
structure module_doc_info  :
Type
source
def ext_tactic_doc_entry.to_tactic_doc_entry (self : ext_tactic_doc_entry) :
tactic_doc_entry
source
structure ext_tactic_doc_entry  :
Type
source
meta def ext_tactic_doc_entry.to_json  :
ext_tactic_doc_entry → json
source
meta def decl_info.to_json  :
decl_info → json
source
meta def format_binders (ns : list name) (bi : binder_info) (t : expr) :
tactic (bool × efmt)
source
meta def binder_info.is_inst_implicit  :
binder_info → bool
source
meta def count_named_intros  :
expr → ℕ
source
meta def get_args_and_type (e : expr) :
tactic (list (bool × efmt) × efmt)
source
meta def attribute_list  :
list name

The attributes we check for

source
meta def attributes_of (n : name) :
tactic (list string)
source
meta def get_proj_type (struct_name proj_name : name) :
tactic efmt
source
meta def mk_structure_fields (decl : name) (e : environment) :
tactic (list (string × efmt))
source
meta def mk_const_with_params (d : declaration) :
expr
source
meta def get_constructor_type (type_name constructor_name : name) :
tactic efmt
source
meta def mk_constructors (decl : name) (e : environment) :
tactic (list (string × efmt))
source
meta def get_equations (decl : name) :
tactic (list efmt)
source
meta def get_kind (d : declaration) :
tactic string
source
meta def process_decl (d : declaration) :
tactic (option decl_info)

extracts decl_info from d. Should return none instead of failing.

source
meta def write_module_doc_pair  :
pos × string → json
source
meta def write_olean_docs  :
tactic (list (string × json))
source
meta def get_instances  :
tactic (native.rb_lmap string string)
source
meta def format_instance_list  :
tactic json
source
meta def format_notes  :
tactic json
source
meta def name.imported_by_tactic_basic (decl_name : name) :
bool
source
meta def name.imported_by_tactic_default (decl_name : name) :
bool
source
meta def name.imported_always (decl_name : name) :
bool
source
meta def tactic_doc_entry.add_import  :
tactic_doc_entry → ext_tactic_doc_entry
source
meta def format_tactic_docs  :
tactic json
source
meta def mk_export_json  :
tactic json
source
meta def open_all_locales (_x : interactive.parse (lean.parser.tk "open_all_locales")) :
lean.parser unit
source
meta def main  :
io unit