feat(library/standard): add markdown documentation

library/standard/data/data.md

@@ -0,0 +1,20 @@
+data
+====
+
+Various datatypes.
+
+Basic types:
+
+* [unit](unit.lean) : the singleton type
+* [bool](bool.lean)
+* [num](num.lean) : generic numerals
+* [string](string.lean) : ascii strings
+* [nat](nat/nat.md) : the natural numbers
+* [int](int/int.md) : the integers
+
+Constructors:
+
+* [option](option.lean)
+* [pair](pair.lean)
+* [list](list/list.md)
+* [set](set.lean)

library/standard/data/list/list.md

@@ -0,0 +1,7 @@
+data.list
+=========
+
+Lists of elements of a fixed type. By default, `import list` imports
+everything here.
+
+[basic](basic.lean) : basic operations and properties

library/standard/data/nat/nat.md

@@ -0,0 +1,6 @@
+data.nat
+========
+
+The natural numbers.
+
+* [nat1](nat1.lean) : a start on the natural numbers

library/standard/logic/axioms/axioms.md

@@ -0,0 +1,11 @@
+logic.axioms
+============
+
+Axioms that extend the Calculus of Constructions.
+
+* [funext](funext.lean) : function extensionality
+* [classical](classical.lean) : the law of the excluded middle
+* [hilbert](hilbert.lean) : choice functions
+* [piext](piext.lean) : equality of Pi types
+* [prop_decidable](prop_decidable.lean) : the decidable class is trivial with excluded middle
+* [examples](examples/examples.md)

library/standard/logic/axioms/examples/examples.md

@@ -0,0 +1,6 @@
+logic.axioms.examples
+=====================
+
+Examples involving the axioms.
+
+* [diaconescu](diaconescu.lean) : Diaconescu's theorem

library/standard/logic/classes/classes.md

@@ -0,0 +1,8 @@
+logic.classes
+=============
+
+Useful classes for general logical manipulations.
+
+* [inhabited](inhabited.lean) : inhabited types
+* [decidable](decidable.lean) : decidable types
+* [congr](congr.lean) : congruences with respect to suitable relations

library/standard/logic/connectives/connectives.md

@@ -0,0 +1,12 @@
+logic.connectives
+=================
+
+Logical operations and connectives.
+
+* [prop](prop.lean) : the type Prop
+* [function](function.lean) : notation for functions
+* [basic](basic.lean) : propositional connectives
+* [eq](eq.lean) : equality and disequality
+* [cast](cast.lean) : casts and heterogeneous equality
+* [quantifiers](quantifiers.lean) : existential and universal quantifiers
+* [if](if.lean) : if-then-else

library/standard/logic/logic.md

@@ -0,0 +1,8 @@
+logic
+=====
+
+Logical constructions and axioms. By default, `import logic` does not import any additional axioms.
+
+* [connectives](connectives/connectives.md) : logical connectives
+* [axioms](axioms/axioms.md) : additional axioms
+* [classes](classes/classes.md) : classes for inhabited types, decidable types, etc.

library/standard/standard.md

@@ -0,0 +1,10 @@
+standard
+========
+
+The Lean standard library. By default, `import standard` does not
+import the classical axioms. For that, use `import logic.axioms`.
+
+* [logic](logic/logic.md) : logical constructs and axioms
+* [data](data/data.md) : various datatypes
+* [struc](struc/struc.md) : axiomatic structures
+* [tools](tools/tool.md) : various additional tools

library/standard/struc/struc.md

@@ -0,0 +1,8 @@
+struc
+=====
+
+Axiomatic properties and structures.
+
+* [binary](binary.lean) : binary operations
+* [equivalence](equivalence.lean) : equivalence relations
+* [wf](wf.lean) : well-founded relations

library/standard/tools/tools.md

@@ -0,0 +1,6 @@
+tools
+=====
+
+Various additional tools.
+
+* [tactic](tactic.lean) : reflected syntax for tactics