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