From 0537ef2bd9a9299ebcfff7588094d34f1f83140e Mon Sep 17 00:00:00 2001 From: Floris van Doorn Date: Sat, 21 Nov 2015 15:12:45 -0500 Subject: [PATCH] chore(*): add me as author to files where I made nontrivial contributions --- hott/init/default.hlean | 2 +- hott/init/equiv.hlean | 2 +- hott/init/funext.hlean | 2 +- hott/init/logic.hlean | 2 +- hott/init/reserved_notation.hlean | 2 +- hott/init/ua.hlean | 2 +- hott/types/list.hlean | 2 +- library/data/list/basic.lean | 2 +- library/data/list/comb.lean | 2 +- library/init/reserved_notation.lean | 2 +- 10 files changed, 10 insertions(+), 10 deletions(-) diff --git a/hott/init/default.hlean b/hott/init/default.hlean index 34281ff85..044ed82da 100644 --- a/hott/init/default.hlean +++ b/hott/init/default.hlean @@ -1,7 +1,7 @@ /- Copyright (c) 2014 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Authors: Leonardo de Moura, Jakob von Raumer +Authors: Leonardo de Moura, Jakob von Raumer, Floris van Doorn -/ prelude diff --git a/hott/init/equiv.hlean b/hott/init/equiv.hlean index d8cdd9196..a1bc4dab2 100644 --- a/hott/init/equiv.hlean +++ b/hott/init/equiv.hlean @@ -1,7 +1,7 @@ /- Copyright (c) 2014 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Author: Jeremy Avigad, Jakob von Raumer +Author: Jeremy Avigad, Jakob von Raumer, Floris van Doorn Ported from Coq HoTT -/ diff --git a/hott/init/funext.hlean b/hott/init/funext.hlean index 331081987..e030ceb28 100644 --- a/hott/init/funext.hlean +++ b/hott/init/funext.hlean @@ -1,7 +1,7 @@ /- Copyright (c) 2014 Jakob von Raumer. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Authors: Jakob von Raumer +Authors: Jakob von Raumer, Floris van Doorn Ported from Coq HoTT -/ diff --git a/hott/init/logic.hlean b/hott/init/logic.hlean index b77d85007..bfeb4bf3c 100644 --- a/hott/init/logic.hlean +++ b/hott/init/logic.hlean @@ -1,7 +1,7 @@ /- Copyright (c) 2014 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Authors: Leonardo de Moura +Authors: Leonardo de Moura, Floris van Doorn -/ prelude diff --git a/hott/init/reserved_notation.hlean b/hott/init/reserved_notation.hlean index 7a39a30de..70de28994 100644 --- a/hott/init/reserved_notation.hlean +++ b/hott/init/reserved_notation.hlean @@ -1,7 +1,7 @@ /- Copyright (c) 2014 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Authors: Leonardo de Moura +Authors: Leonardo de Moura, Floris van Doorn -/ prelude import init.datatypes diff --git a/hott/init/ua.hlean b/hott/init/ua.hlean index f0981462c..fba2c1dd5 100644 --- a/hott/init/ua.hlean +++ b/hott/init/ua.hlean @@ -1,7 +1,7 @@ /- Copyright (c) 2014 Jakob von Raumer. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Author: Jakob von Raumer +Authors: Jakob von Raumer, Floris van Doorn Ported from Coq HoTT -/ diff --git a/hott/types/list.hlean b/hott/types/list.hlean index b1e9eb822..2ea8b8600 100644 --- a/hott/types/list.hlean +++ b/hott/types/list.hlean @@ -1,7 +1,7 @@ /- 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 +Authors: Parikshit Khanna, Jeremy Avigad, Leonardo de Moura, Floris van Doorn Basic properties of lists. Ported from the standard library (list.basic and list.comb) diff --git a/library/data/list/basic.lean b/library/data/list/basic.lean index 66b92f12b..619c23684 100644 --- a/library/data/list/basic.lean +++ b/library/data/list/basic.lean @@ -1,7 +1,7 @@ /- 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 +Authors: Parikshit Khanna, Jeremy Avigad, Leonardo de Moura, Floris van Doorn Basic properties of lists. -/ diff --git a/library/data/list/comb.lean b/library/data/list/comb.lean index b4ebdb4fb..d3c47c565 100644 --- a/library/data/list/comb.lean +++ b/library/data/list/comb.lean @@ -1,7 +1,7 @@ /- 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 +Authors: Leonardo de Moura, Haitao Zhang, Floris van Doorn List combinators. -/ diff --git a/library/init/reserved_notation.lean b/library/init/reserved_notation.lean index 073b0e820..7741e12ed 100644 --- a/library/init/reserved_notation.lean +++ b/library/init/reserved_notation.lean @@ -1,7 +1,7 @@ /- Copyright (c) 2014 Microsoft Corporation. All rights reserved. Released under Apache 2.0 license as described in the file LICENSE. -Authors: Leonardo de Moura, Jeremy Avigad +Authors: Leonardo de Moura, Jeremy Avigad, Floris van Doorn -/ prelude import init.datatypes