2022-02-13 14:42:15 +00:00
|
|
|
import DocGen4.Output.Template
|
|
|
|
|
|
|
|
|
|
namespace DocGen4
|
|
|
|
|
namespace Output
|
|
|
|
|
|
|
|
|
|
open scoped DocGen4.Jsx
|
|
|
|
|
open Lean
|
|
|
|
|
|
2022-07-20 23:40:04 +00:00
|
|
|
def find : BaseHtmlM Html := do
|
2022-02-20 17:12:49 +00:00
|
|
|
pure
|
|
|
|
|
<html lang="en">
|
|
|
|
|
<head>
|
2023-01-01 18:51:01 +00:00
|
|
|
<link rel="preload" href={s!"{← getRoot}/declarations/declaration-data.bmp"} as="image"/>
|
|
|
|
|
<script>{s!"const SITE_ROOT={String.quote (← getRoot)};"}</script>
|
2022-07-20 23:40:04 +00:00
|
|
|
<script type="module" async="true" src="./find.js"></script>
|
2022-02-20 17:12:49 +00:00
|
|
|
</head>
|
|
|
|
|
<body></body>
|
|
|
|
|
</html>
|
|
|
|
|
|
2022-02-13 14:42:15 +00:00
|
|
|
end Output
|
|
|
|
|
end DocGen4
|
2022-02-20 17:12:49 +00:00
|
|
|
|
