From e4b9a89f5ffa7b69e293c630439ec99fe20b28aa Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Tue, 13 Jan 2015 16:35:59 -0800 Subject: [PATCH] refactor(library/data/fin): remove unnecessary import --- library/data/fin.lean | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/library/data/fin.lean b/library/data/fin.lean index abd2b2d7fc..dcb9f35811 100644 --- a/library/data/fin.lean +++ b/library/data/fin.lean @@ -7,7 +7,7 @@ Author: Leonardo de Moura Finite ordinals. -/ -import data.nat logic.cast +import data.nat open nat inductive fin : nat → Type :=