diff --git a/library/init/option.lean b/library/init/option.lean index 56f144ff82..ccfa0d3e7d 100644 --- a/library/init/option.lean +++ b/library/init/option.lean @@ -2,8 +2,6 @@ Copyright (c) 2014 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. Authors: Leonardo de Moura - -Basic datatypes -/ prelude import init.logic init.monad init.alternative