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

chore(library/data/list): add back copyright notice

Browse source
This commit is contained in:
Joe Hendrix 2017-01-05 23:54:32 -08:00 • committed by Leonardo de Moura
parent 24fc68cef4
commit 985c3697b9
3 changed files with 19 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
library/data/list/basic.lean
View file

@ -1,3 +1,10 @@
/-
Copyright (c) 2014 Parikshit Khanna. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Parikshit Khanna, Jeremy Avigad, Leonardo de Moura, Floris van Doorn
Basic properties of lists.
-/
import init.data.list.basic
import data.nat.order

7
library/data/list/comb.lean
View file

@ -1,3 +1,10 @@
/-
Copyright (c) 2015 Leonardo de Moura. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura, Haitao Zhang, Floris van Doorn
List combinators.
-/
import init.data.list.basic
import data.nat.order

5
library/data/list/default.lean
View file

@ -1 +1,6 @@
/-
Copyright (c) 2014 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Jeremy Avigad
-/
import .basic .comb