From 6829f5e3bda44ff0f367692abe746bec71137969 Mon Sep 17 00:00:00 2001 From: David Thrane Christiansen Date: Fri, 5 Apr 2024 15:20:42 +0200 Subject: [PATCH] Add missing docstrings --- src/verso-manual/Verso/Genre/Manual/Basic.lean | 6 ++++++ src/verso-manual/Verso/Genre/Manual/Docstring.lean | 6 ++++++ 2 files changed, 12 insertions(+) diff --git a/src/verso-manual/Verso/Genre/Manual/Basic.lean b/src/verso-manual/Verso/Genre/Manual/Basic.lean index 5809cd7..3b50c24 100644 --- a/src/verso-manual/Verso/Genre/Manual/Basic.lean +++ b/src/verso-manual/Verso/Genre/Manual/Basic.lean @@ -1,3 +1,9 @@ +/- +Copyright (c) 2024 Lean FRO LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Author: David Thrane Christiansen +-/ + import Lean import Verso.Doc import Verso.Doc.Html diff --git a/src/verso-manual/Verso/Genre/Manual/Docstring.lean b/src/verso-manual/Verso/Genre/Manual/Docstring.lean index fc24b65..8b11cee 100644 --- a/src/verso-manual/Verso/Genre/Manual/Docstring.lean +++ b/src/verso-manual/Verso/Genre/Manual/Docstring.lean @@ -1,3 +1,9 @@ +/- +Copyright (c) 2024 Lean FRO LLC. All rights reserved. +Released under Apache 2.0 license as described in the file LICENSE. +Author: David Thrane Christiansen +-/ + import Lean import Verso.Genre.Manual.Basic import Verso.Doc.Elab.Monad