From 26ad6dde69dbadfaaa65a8e0480bae0ce27d0c54 Mon Sep 17 00:00:00 2001 From: Jeremy Avigad Date: Sat, 16 May 2015 17:51:50 +1000 Subject: [PATCH] fix(library/data/fintype.lean): reduce imports, to avoid cyclic dependencies --- library/data/fintype.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/library/data/fintype.lean b/library/data/fintype.lean index 714e512b2e..b369594360 100644 --- a/library/data/fintype.lean +++ b/library/data/fintype.lean @@ -5,7 +5,7 @@ Authors: Leonardo de Moura Finite type (type class). -/ -import data.list data.bool +import data.list.perm data.list.as_type data.bool open list bool unit decidable option function structure fintype [class] (A : Type) : Type :=