From 929a536e2f9268788187c3da09986673981b4466 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 6 Jan 2014 12:03:11 -0800 Subject: [PATCH] fix(builtin/README): update documentation Signed-off-by: Leonardo de Moura --- src/builtin/README.md | 14 +++++++++++--- 1 file changed, 11 insertions(+), 3 deletions(-) diff --git a/src/builtin/README.md b/src/builtin/README.md index 85c85ce2d..c5ab6025c 100644 --- a/src/builtin/README.md +++ b/src/builtin/README.md @@ -1,4 +1,12 @@ -Extra functionality -------------------- +Builtin libraries and scripts +------------------------------ + +This directory contains builtin Lean theories and additional Lua +scripts that are distributed with Lean. Some of the theories (e.g., +`kernel.lean`) are automatically loaded when we start Lean. Others +must be imported using the `import` command. + +Several Lean components rely on these libraries. For example, they use +the axioms and theorems defined in these libraries to build proofs. + -This directory contains Lean theories and additional Lua scripts.