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).
+-/