max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore(library/init/option): remove bad comment

Browse source
This commit is contained in:
Leonardo de Moura 2016-07-22 11:36:33 -07:00
parent eb526be99f
commit 9aebb168a3
1 changed files with 0 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
library/init/option.lean
View file

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