michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

fix(library/data/fintype.lean): reduce imports, to avoid cyclic dependencies

Browse source
This commit is contained in:
Jeremy Avigad 2015-05-16 17:51:50 +10:00
parent daf53e4de2
commit 26ad6dde69
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
library/data/fintype.lean
View file

@ -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 :=