michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

fix(hott/*.md,library/*.md): use the word 'file' instead of 'module'

Browse source
This commit is contained in:
Jeremy Avigad 2015-05-24 18:36:26 +10:00 committed by Leonardo de Moura
parent 6db08c5519
commit 716da2488b
4 changed files with 4 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
hott/hott.md
View file

@ -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

2
hott/init/init.md
View file

@ -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".

2
library/init/init.md
View file

@ -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".

2
library/library.md
View file

@ -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