From 985c3697b9ae10452e64a15082e3cc2cfa7b9701 Mon Sep 17 00:00:00 2001 From: Joe Hendrix Date: Thu, 5 Jan 2017 23:54:32 -0800 Subject: [PATCH] chore(library/data/list): add back copyright notice --- library/data/list/basic.lean | 7 +++++++ library/data/list/comb.lean | 7 +++++++ library/data/list/default.lean | 5 +++++ 3 files changed, 19 insertions(+) diff --git a/library/data/list/basic.lean b/library/data/list/basic.lean index 51fa63b26c..85b6d2bdb3 100644 --- a/library/data/list/basic.lean +++ b/library/data/list/basic.lean @@ -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 diff --git a/library/data/list/comb.lean b/library/data/list/comb.lean index b70bb9d4c8..c5c9be34ed 100644 --- a/library/data/list/comb.lean +++ b/library/data/list/comb.lean @@ -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 diff --git a/library/data/list/default.lean b/library/data/list/default.lean index 55928ebb0f..ea15318b99 100644 --- a/library/data/list/default.lean +++ b/library/data/list/default.lean @@ -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