bookshelf-doc/DocGen4/Output/Index.lean

26 lines
806 B
Plaintext
Raw Normal View History

/-
Copyright (c) 2021 Henrik Böving. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Henrik Böving
-/
2022-05-19 18:36:35 +00:00
import DocGen4.Output.ToHtmlFormat
import DocGen4.Output.Template
namespace DocGen4
namespace Output
open scoped DocGen4.Jsx
2022-07-23 11:01:25 +00:00
def index : BaseHtmlM Html := do templateExtends (baseHtml "Index") <|
pure <|
<main>
<a id="top"></a>
<h1> Welcome to the documentation page </h1>
2023-03-11 16:48:27 +00:00
-- Temporary comment until the lake issue is resolved
-- for commit <a href={s!"{← getProjectGithubUrl}/tree/{← getProjectCommit}"}>{s!"{← getProjectCommit} "}</a>
<p>This was built using Lean 4 at commit <a href={s!"https://github.com/leanprover/lean4/tree/{Lean.githash}"}>{Lean.githash}</a></p>
2022-07-23 11:01:25 +00:00
</main>
end Output
end DocGen4