diff --git a/library/data/quotient/default.lean b/library/data/quotient/default.lean index 22d38eec9..9c1431474 100644 --- a/library/data/quotient/default.lean +++ b/library/data/quotient/default.lean @@ -2,4 +2,4 @@ --- Released under Apache 2.0 license as described in the file LICENSE. --- Author: Jeremy Avigad -import .basic .classical +import .basic