From 0fb398c21750e0e5e52f11aaa9bd68653dcb4cef Mon Sep 17 00:00:00 2001 From: Jeremy Avigad Date: Thu, 31 Dec 2015 13:23:52 -0800 Subject: [PATCH] fix(library/data/nat/bigops): delete some blank lines --- library/data/nat/bigops.lean | 4 ---- 1 file changed, 4 deletions(-) diff --git a/library/data/nat/bigops.lean b/library/data/nat/bigops.lean index cb97ca40d8..4ff5416ccb 100644 --- a/library/data/nat/bigops.lean +++ b/library/data/nat/bigops.lean @@ -192,8 +192,4 @@ proposition prod_range_offset (m n : ℕ) (f : ℕ → A) : end set - - - - end nat