From f6ba6da4b518aa231bb1eee543c2463f3d3c3040 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Thu, 7 Aug 2014 17:52:51 -0700 Subject: [PATCH] fix(library/standard): add missing 'end' of namespace Signed-off-by: Leonardo de Moura --- library/standard/data/list/basic.lean | 2 ++ library/standard/data/nat/basic.lean | 1 + library/standard/logic/classes/congr.lean | 1 + 3 files changed, 4 insertions(+) diff --git a/library/standard/data/list/basic.lean b/library/standard/data/list/basic.lean index 091123f29..7a4566f14 100644 --- a/library/standard/data/list/basic.lean +++ b/library/standard/data/list/basic.lean @@ -288,3 +288,5 @@ end -- declare global notation outside the section infixl `++` : 65 := concat + +end list \ No newline at end of file diff --git a/library/standard/data/nat/basic.lean b/library/standard/data/nat/basic.lean index 900bf6ac6..e9c9eb191 100644 --- a/library/standard/data/nat/basic.lean +++ b/library/standard/data/nat/basic.lean @@ -415,3 +415,4 @@ discriminate -- add_rewrite mul_succ_left mul_succ_right -- add_rewrite mul_comm mul_assoc mul_left_comm -- add_rewrite mul_distr_right mul_distr_left +end nat \ No newline at end of file diff --git a/library/standard/logic/classes/congr.lean b/library/standard/logic/classes/congr.lean index 6f2446eaa..00303fdaf 100644 --- a/library/standard/logic/classes/congr.lean +++ b/library/standard/logic/classes/congr.lean @@ -137,3 +137,4 @@ calc ... ↔ (a ∨ c) ∨ b : iff_symm (or_assoc _ _ _) -- TODO: add or_left_comm, and_right_comm, and_left_comm +end congr \ No newline at end of file