Skip to content

Commit 598a690

Browse files
author
Martin Ceresa
committed
added docs html
1 parent 0e8b282 commit 598a690

2,903 files changed

Lines changed: 423716 additions & 0 deletions

File tree

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

docs/404.html

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
<html lang="en"><head><meta charset="UTF-8"></meta><meta name="viewport" content="width=device-width, initial-scale=1"></meta><link rel="stylesheet" href="./style.css"></link><link rel="icon" href="./favicon.svg"></link><link rel="mask-icon" href="./favicon.svg" color="#000000"></link><link rel="prefetch" href=".//declarations/declaration-data.bmp" as="image"></link><title>404</title><script defer="true" src="./mathjax-config.js"></script><script defer="true" src="https://cdnjs.cloudflare.com/polyfill/v3/polyfill.min.js?features=es6"></script><script defer="true" src="https://cdn.jsdelivr.net/npm/mathjax@3/es5/tex-mml-chtml.js"></script><script>const SITE_ROOT="./";</script><script type="module" src="./jump-src.js"></script><script type="module" src="./search.js"></script><script type="module" src="./expand-nav.js"></script><script type="module" src="./how-about.js"></script><script type="module" src="./instances.js"></script><script type="module" src="./importedBy.js"></script></head><body><input id="nav_toggle" type="checkbox"></input><header><h1><label for="nav_toggle"></label><span>Documentation</span></h1><h2 class="header_filename break_within"><span class="name">404</span></h2><form id="search_form"><input type="text" name="q" autocomplete="off"></input>&#32;<button id="search_button" onclick="javascript: form.action='./search.html';">Search</button></form></header><main><h1>404 Not Found</h1><p>Unfortunately, the page you were looking for is no longer here. </p><div id="howabout"></div></main><nav class="nav"><iframe src="./navbar.html" class="navframe" frameBorder="0"></iframe></nav></body></html>

docs/Aesop.html

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,3 @@
1+
<html lang="en"><head><meta charset="UTF-8"></meta><meta name="viewport" content="width=device-width, initial-scale=1"></meta><link rel="stylesheet" href="./style.css"></link><link rel="icon" href="./favicon.svg"></link><link rel="mask-icon" href="./favicon.svg" color="#000000"></link><link rel="prefetch" href=".//declarations/declaration-data.bmp" as="image"></link><title>Aesop</title><script defer="true" src="./mathjax-config.js"></script><script defer="true" src="https://cdnjs.cloudflare.com/polyfill/v3/polyfill.min.js?features=es6"></script><script defer="true" src="https://cdn.jsdelivr.net/npm/mathjax@3/es5/tex-mml-chtml.js"></script><script>const SITE_ROOT="./";</script><script>const MODULE_NAME="Aesop";</script><script type="module" src="./jump-src.js"></script><script type="module" src="./search.js"></script><script type="module" src="./expand-nav.js"></script><script type="module" src="./how-about.js"></script><script type="module" src="./instances.js"></script><script type="module" src="./importedBy.js"></script></head><body><input id="nav_toggle" type="checkbox"></input><header><h1><label for="nav_toggle"></label><span>Documentation</span></h1><h2 class="header_filename break_within"><span class="name">Aesop</span></h2><form id="search_form"><input type="text" name="q" autocomplete="off"></input>&#32;<button id="search_button" onclick="javascript: form.action='./search.html';">Search</button></form></header><nav class="internal_nav"><p><a href="#top">return to top</a></p><p class="gh_nav_link"><a href="https://github.com/leanprover-community/aesop/blob/471ff276892c3451a1d693477107e9c3a0c8ab85/Aesop.lean">source</a></p><div class="imports"><details><summary>Imports</summary><ul><li><a href="./Init.html">Init</a></li><li><a href="./Aesop/BuiltinRules.html">Aesop.BuiltinRules</a></li><li><a href="./Aesop/Main.html">Aesop.Main</a></li><li><a href="./Aesop/Frontend/Command.html">Aesop.Frontend.Command</a></li><li><a href="./Aesop/Frontend/Saturate.html">Aesop.Frontend.Saturate</a></li></ul></details><details><summary>Imported by</summary><ul id="imported-by-Aesop" class="imported-by-list"></ul></details></div></nav><main>
2+
</main>
3+
<nav class="nav"><iframe src="./navbar.html" class="navframe" frameBorder="0"></iframe></nav></body></html>

docs/Aesop.html.hash

Lines changed: 1 addition & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1 @@
1+
18299745097219060950

docs/Aesop.html.trace

Lines changed: 5 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,5 @@
1+
{"log":
2+
[{"message":
3+
".> ELAN=elan ELAN_HOME=/home/martin/.elan ELAN_TOOLCHAIN=leanprover/lean4:v4.18.0-rc1 LAKE=/home/martin/.elan/toolchains/leanprover--lean4---v4.18.0-rc1/bin/lake LAKE_HOME=/home/martin/.elan/toolchains/leanprover--lean4---v4.18.0-rc1 LAKE_PKG_URL_MAP={} LEAN=/home/martin/.elan/toolchains/leanprover--lean4---v4.18.0-rc1/bin/lean LEAN_GITHASH=69a1d0485e241a494d69d3e2c98ad988f4396dcd LEAN_SYSROOT=/home/martin/.elan/toolchains/leanprover--lean4---v4.18.0-rc1 LEAN_AR=/home/martin/.elan/toolchains/leanprover--lean4---v4.18.0-rc1/bin/llvm-ar LEAN_CC= LEAN_PATH=././../.lake/packages/batteries/.lake/build/lib/lean:././../.lake/packages/Qq/.lake/build/lib/lean:././../.lake/packages/aesop/.lake/build/lib/lean:././../.lake/packages/proofwidgets/.lake/build/lib/lean:././../.lake/packages/importGraph/.lake/build/lib/lean:././../.lake/packages/LeanSearchClient/.lake/build/lib/lean:././../.lake/packages/plausible/.lake/build/lib/lean:././../.lake/packages/mathlib/.lake/build/lib/lean:././../.lake/packages/MD4Lean/.lake/build/lib/lean:././../.lake/packages/BibtexQuery/.lake/build/lib/lean:././../.lake/packages/UnicodeBasic/.lake/build/lib/lean:././../.lake/packages/Cli/.lake/build/lib/lean:./././..//.lake/build/lib/lean:././../.lake/packages/doc-gen4/.lake/build/lib/lean:././.lake/build/lib/lean:/home/martin/.elan/toolchains/leanprover--lean4---v4.18.0-rc1/lib/lean LEAN_SRC_PATH=././../.lake/packages/batteries/./.:././../.lake/packages/batteries/./.:././../.lake/packages/Qq/./.:././../.lake/packages/aesop/./.:././../.lake/packages/aesop/./.:././../.lake/packages/proofwidgets/./.:././../.lake/packages/proofwidgets/./.:././../.lake/packages/importGraph/./.:././../.lake/packages/importGraph/./.:././../.lake/packages/LeanSearchClient/./.:././../.lake/packages/LeanSearchClient/./.:././../.lake/packages/plausible/./.:././../.lake/packages/plausible/./.:././../.lake/packages/mathlib/./.:././../.lake/packages/mathlib/./.:././../.lake/packages/mathlib/./.:././../.lake/packages/mathlib/./.:././../.lake/packages/mathlib/./.:././../.lake/packages/mathlib/./.:././../.lake/packages/mathlib/./.:././../.lake/packages/MD4Lean/./.:././../.lake/packages/MD4Lean/./.:././../.lake/packages/BibtexQuery/./.:././../.lake/packages/UnicodeBasic/./.:././../.lake/packages/UnicodeBasic/./.:././../.lake/packages/Cli/./.:./././..//./.:././../.lake/packages/doc-gen4/./.:/home/martin/.elan/toolchains/leanprover--lean4---v4.18.0-rc1/src/lean/lake PATH LD_LIBRARY_PATH=././.lake/build/lib:././../.lake/packages/doc-gen4/.lake/build/lib:./././..//.lake/build/lib:././../.lake/packages/Cli/.lake/build/lib:././../.lake/packages/UnicodeBasic/.lake/build/lib:././../.lake/packages/BibtexQuery/.lake/build/lib:././../.lake/packages/MD4Lean/.lake/build/lib:././../.lake/packages/mathlib/.lake/build/lib:././../.lake/packages/plausible/.lake/build/lib:././../.lake/packages/LeanSearchClient/.lake/build/lib:././../.lake/packages/importGraph/.lake/build/lib:././../.lake/packages/proofwidgets/.lake/build/lib:././../.lake/packages/aesop/.lake/build/lib:././../.lake/packages/Qq/.lake/build/lib:././../.lake/packages/batteries/.lake/build/lib:/home/martin/.elan/toolchains/leanprover--lean4---v4.18.0-rc1/lib/lean:/home/martin/.elan/toolchains/leanprover--lean4---v4.18.0-rc1/lib ././../.lake/packages/doc-gen4/.lake/build/bin/doc-gen4 single --build ././.lake/build Aesop https://github.com/leanprover-community/aesop/blob/471ff276892c3451a1d693477107e9c3a0c8ab85/Aesop.lean",
4+
"level": "trace"}],
5+
"depHash": "6702438519377605506"}

0 commit comments

Comments
 (0)