max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

doc(fixing_broken_links)

Browse source 
A stopgap fix for broken links in `library.md`. Addresses #1649 for now.
This commit is contained in:
Scott Morrison 2017-03-21 23:08:15 +11:00 • committed by Leonardo de Moura
parent 875493a1ee
commit d6f5370ea7
1 changed files with 6 additions and 9 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

15
library/library.md
View file

@ -1,14 +1,14 @@
The Lean Standard Library
=========================
(This documentation is partially out-of-date.)
The Lean standard library is contained in the following files and directories:
* [init](init/init.md) : constants and theorems needed for low-level system operations
* [logic](logic/logic.md) : logical constructs and axioms
* [data](data/data.md) : concrete datatypes and type constructors
* [algebra](algebra/algebra.md) : algebraic structures
* [theories](theories/theories.md) : more domain-specific theories
* [tools](tools/tools.md) : additional tools
* [init](init/) : constants and theorems needed for low-level system operations
* [init/logic.lean](init/logic.lean) : logical constructs and axioms
* [init/data](init/data/) : concrete datatypes and type constructors
* [init/algebra](init/algebra/) : algebraic structures
* [tools](tools/) : additional tools
The files in `init` are loaded by default, and hence do not need to be
imported manually. Other files can be imported individually, but the
@ -47,6 +47,3 @@ sparingly. For example:
You can use `print axioms foo` to see which axioms `foo` depends
on. Many of the theories in the `theories` folder are unreservedly
classical.
See also the [hott library](../hott/hott.md), a library for homotopy
type theory based on a predicative foundation.