From dc2b905a7c5bd2ad27e943f30326c970c4bedad2 Mon Sep 17 00:00:00 2001 From: Floris van Doorn Date: Thu, 30 Mar 2017 18:33:33 -0400 Subject: [PATCH] rename module to left_module --- algebra/graded.hlean | 4 ++-- algebra/{module.hlean => left_module.hlean} | 0 algebra/module_chain_complex.hlean | 2 +- known_bugs.txt | 1 + 4 files changed, 4 insertions(+), 3 deletions(-) rename algebra/{module.hlean => left_module.hlean} (100%) diff --git a/algebra/graded.hlean b/algebra/graded.hlean index 30c486a..e90ff88 100644 --- a/algebra/graded.hlean +++ b/algebra/graded.hlean @@ -1,8 +1,8 @@ -/- Graded modules -/ +/- Graded (left-) R-modules for a ring R. -/ -- Author: Floris van Doorn -import ..algebra.module +import .left_module open algebra eq left_module pointed function equiv is_equiv is_trunc prod diff --git a/algebra/module.hlean b/algebra/left_module.hlean similarity index 100% rename from algebra/module.hlean rename to algebra/left_module.hlean diff --git a/algebra/module_chain_complex.hlean b/algebra/module_chain_complex.hlean index 9993f55..8032140 100644 --- a/algebra/module_chain_complex.hlean +++ b/algebra/module_chain_complex.hlean @@ -1,7 +1,7 @@ /- Author: Jeremy Avigad -/ -import homotopy.chain_complex ..algebra.module ..algebra.is_short_exact ..move_to_lib +import homotopy.chain_complex .left_module .is_short_exact ..move_to_lib open eq pointed sigma fiber equiv is_equiv sigma.ops is_trunc nat trunc open algebra function open chain_complex diff --git a/known_bugs.txt b/known_bugs.txt index f44968f..140de9d 100644 --- a/known_bugs.txt +++ b/known_bugs.txt @@ -6,6 +6,7 @@ instead of - When using the calc mode for homotopies, you have to give the proofs using a tactic (e.g. `by exact foo` instead of `foo`) +- A file named "module.hlean" cannot be imported using `import .module` because `module` is a keyword (but it can be imported using `import ..foo.module`) Issues which are not bugs, but still good to know