From 716da2488b97830d4b37b6de22518b2527626a8e Mon Sep 17 00:00:00 2001 From: Jeremy Avigad Date: Sun, 24 May 2015 18:36:26 +1000 Subject: [PATCH] fix(hott/*.md,library/*.md): use the word 'file' instead of 'module' --- hott/hott.md | 2 +- hott/init/init.md | 2 +- library/init/init.md | 2 +- library/library.md | 2 +- 4 files changed, 4 insertions(+), 4 deletions(-) diff --git a/hott/hott.md b/hott/hott.md index e9548f8c0..0076f1729 100644 --- a/hott/hott.md +++ b/hott/hott.md @@ -2,7 +2,7 @@ The Lean Homotopy Type Theory Library ===================================== The Lean homotopy type theory library is contained in the following -modules and directories: +files and directories: * [init](init/init.md) : constants and theorems needed for low-level system operations * [types](types/types.md) : concrete datatypes and type constructors diff --git a/hott/init/init.md b/hott/init/init.md index bb5912de7..cae694a9f 100644 --- a/hott/init/init.md +++ b/hott/init/init.md @@ -1,7 +1,7 @@ init ==== -The modules in this folder are required by low-level operations, and +The files in this folder are required by low-level operations, and are always imported by default. You can suppress this behavior by beginning a file with the keyword "prelude". diff --git a/library/init/init.md b/library/init/init.md index ce5d86c8b..7fb27f16e 100644 --- a/library/init/init.md +++ b/library/init/init.md @@ -1,7 +1,7 @@ init ==== -The modules in this folder are required by low-level operations, and +The files in this folder are required by low-level operations, and are always imported by default. You can suppress this behavior by beginning a file with the keyword "prelude". diff --git a/library/library.md b/library/library.md index 2f27024c5..cafdebe4d 100644 --- a/library/library.md +++ b/library/library.md @@ -1,7 +1,7 @@ The Lean Standard Library ========================= -The Lean standard library is contained in the following modules and directories: +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