From c841e63649cf4e815ccf1e1ca61060f144c2b658 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Wed, 3 Jun 2015 16:43:55 -0700
Subject: [PATCH] refactor(library/data/fintype): create 'fintype' subdirectory

---
 library/data/{fintype.lean => fintype/basic.lean} | 0
 library/data/fintype/default.lean                 | 8 ++++++++
 library/data/fintype/function.lean                | 7 +++++++
 3 files changed, 15 insertions(+)
 rename library/data/{fintype.lean => fintype/basic.lean} (100%)
 create mode 100644 library/data/fintype/default.lean
 create mode 100644 library/data/fintype/function.lean

diff --git a/library/data/fintype.lean b/library/data/fintype/basic.lean
similarity index 100%
rename from library/data/fintype.lean
rename to library/data/fintype/basic.lean
diff --git a/library/data/fintype/default.lean b/library/data/fintype/default.lean
new file mode 100644
index 000000000..48054d0c3
--- /dev/null
+++ b/library/data/fintype/default.lean
@@ -0,0 +1,8 @@
+/-
+Copyright (c) 2015 Leonardo de Moura. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+
+Finite type (type class).
+-/
+import data.fintype.basic data.fintype.function
diff --git a/library/data/fintype/function.lean b/library/data/fintype/function.lean
new file mode 100644
index 000000000..825ed4d7c
--- /dev/null
+++ b/library/data/fintype/function.lean
@@ -0,0 +1,7 @@
+/-
+Copyright (c) 2015 Haitao Zhang. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Haitao Zhang
+
+Finite type (type class).
+-/