Skip to content

Commit 743307c

Browse files
SmaniaDSmaniaD
committed
Update generated documentation
1 parent 4bc9bc0 commit 743307c

4,928 files changed

Lines changed: 2555296 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/f0c6e183ea26531e82773feb4b73ab6595ca17a5/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/Frontend.html">Aesop.Frontend</a></li><li><a href="./Aesop/Main.html">Aesop.Main</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/BaseM.html‎

Lines changed: 30 additions & 0 deletions
Large diffs are not rendered by default.

‎docs/Aesop/Builder/Apply.html‎

Lines changed: 29 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -0,0 +1,29 @@
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.Builder.Apply</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.Builder.Apply";</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>.<span class="name">Builder</span>.<span class="name">Apply</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/f0c6e183ea26531e82773feb4b73ab6595ca17a5/Aesop/Builder/Apply.lean">source</a></p><div class="imports"><details><summary>Imports</summary><ul><li><a href="../.././Init.html">Init</a></li><li><a href="../.././Aesop/Builder/Basic.html">Aesop.Builder.Basic</a></li></ul></details><details><summary>Imported by</summary><ul id="imported-by-Aesop.Builder.Apply" class="imported-by-list"></ul></details></div><div class="nav_link"><a class="break_within" href="#Aesop.RuleBuilderOptions.applyTransparency"><span class="name">Aesop</span>.<span class="name">RuleBuilderOptions</span>.<span class="name">applyTransparency</span></a></div><div class="nav_link"><a class="break_within" href="#Aesop.RuleBuilderOptions.applyIndexTransparency"><span class="name">Aesop</span>.<span class="name">RuleBuilderOptions</span>.<span class="name">applyIndexTransparency</span></a></div><div class="nav_link"><a class="break_within" href="#Aesop.RuleBuilder.getApplyIndexingMode"><span class="name">Aesop</span>.<span class="name">RuleBuilder</span>.<span class="name">getApplyIndexingMode</span></a></div><div class="nav_link"><a class="break_within" href="#Aesop.RuleBuilder.checkNoIff"><span class="name">Aesop</span>.<span class="name">RuleBuilder</span>.<span class="name">checkNoIff</span></a></div><div class="nav_link"><a class="break_within" href="#Aesop.RuleBuilder.applyCore"><span class="name">Aesop</span>.<span class="name">RuleBuilder</span>.<span class="name">applyCore</span></a></div><div class="nav_link"><a class="break_within" href="#Aesop.RuleBuilder.apply"><span class="name">Aesop</span>.<span class="name">RuleBuilder</span>.<span class="name">apply</span></a></div></nav><main>
2+
<div class="decl" id="Aesop.RuleBuilderOptions.applyTransparency"><div class="def"><div class="gh_link"><a href="https://github.com/leanprover-community/aesop/blob/f0c6e183ea26531e82773feb4b73ab6595ca17a5/Aesop/Builder/Apply.lean#L19-L20">source</a></div><div class="decl_header"><span class="decl_kind">def</span>
3+
<span class="decl_name"><a class="break_within" href="../.././Aesop/Builder/Apply.html#Aesop.RuleBuilderOptions.applyTransparency"><span class="name">Aesop</span>.<span class="name">RuleBuilderOptions</span>.<span class="name">applyTransparency</span></a></span><span class="decl_args">
4+
<span class="fn">(<span class="fn">opts</span> : <a href="../.././Aesop/Builder/Basic.html#Aesop.RuleBuilderOptions">RuleBuilderOptions</a>)</span></span>
5+
<span class="decl_args"> :</span><div class="decl_type"><a href="../.././Init/MetaTypes.html#Lean.Meta.TransparencyMode">Lean.Meta.TransparencyMode</a></div></div><details><summary>Equations</summary><ul class="equations"><li class="equation"><span class="fn"><span class="fn">opts</span>.<a href="../.././Aesop/Builder/Apply.html#Aesop.RuleBuilderOptions.applyTransparency">applyTransparency</a></span> <a href="../.././Init/Prelude.html#Eq">=</a> <span class="fn"><span class="fn"><span class="fn"><span class="fn">opts</span>.<a href="../.././Aesop/Builder/Basic.html#Aesop.RuleBuilderOptions.transparency?">transparency?</a></span>.<a href="../.././Init/Prelude.html#Option.getD">getD</a></span> <a href="../.././Init/MetaTypes.html#Lean.Meta.TransparencyMode.default">Lean.Meta.TransparencyMode.default</a></span></li></ul></details><details id="instances-for-list-Aesop.RuleBuilderOptions.applyTransparency" class="instances-for-list"><summary>Instances For</summary><ul class="instances-for-enum"></ul></details></div></div><div class="decl" id="Aesop.RuleBuilderOptions.applyIndexTransparency"><div class="def"><div class="gh_link"><a href="https://github.com/leanprover-community/aesop/blob/f0c6e183ea26531e82773feb4b73ab6595ca17a5/Aesop/Builder/Apply.lean#L22-L23">source</a></div><div class="decl_header"><span class="decl_kind">def</span>
6+
<span class="decl_name"><a class="break_within" href="../.././Aesop/Builder/Apply.html#Aesop.RuleBuilderOptions.applyIndexTransparency"><span class="name">Aesop</span>.<span class="name">RuleBuilderOptions</span>.<span class="name">applyIndexTransparency</span></a></span><span class="decl_args">
7+
<span class="fn">(<span class="fn">opts</span> : <a href="../.././Aesop/Builder/Basic.html#Aesop.RuleBuilderOptions">RuleBuilderOptions</a>)</span></span>
8+
<span class="decl_args"> :</span><div class="decl_type"><a href="../.././Init/MetaTypes.html#Lean.Meta.TransparencyMode">Lean.Meta.TransparencyMode</a></div></div><details><summary>Equations</summary><ul class="equations"><li class="equation"><span class="fn"><span class="fn">opts</span>.<a href="../.././Aesop/Builder/Apply.html#Aesop.RuleBuilderOptions.applyIndexTransparency">applyIndexTransparency</a></span> <a href="../.././Init/Prelude.html#Eq">=</a> <span class="fn"><span class="fn"><span class="fn"><span class="fn">opts</span>.<a href="../.././Aesop/Builder/Basic.html#Aesop.RuleBuilderOptions.indexTransparency?">indexTransparency?</a></span>.<a href="../.././Init/Prelude.html#Option.getD">getD</a></span> <a href="../.././Init/MetaTypes.html#Lean.Meta.TransparencyMode.reducible">Lean.Meta.TransparencyMode.reducible</a></span></li></ul></details><details id="instances-for-list-Aesop.RuleBuilderOptions.applyIndexTransparency" class="instances-for-list"><summary>Instances For</summary><ul class="instances-for-enum"></ul></details></div></div><div class="decl" id="Aesop.RuleBuilder.getApplyIndexingMode"><div class="def"><div class="gh_link"><a href="https://github.com/leanprover-community/aesop/blob/f0c6e183ea26531e82773feb4b73ab6595ca17a5/Aesop/Builder/Apply.lean#L29-L34">source</a></div><div class="decl_header"><span class="decl_kind">def</span>
9+
<span class="decl_name"><a class="break_within" href="../.././Aesop/Builder/Apply.html#Aesop.RuleBuilder.getApplyIndexingMode"><span class="name">Aesop</span>.<span class="name">RuleBuilder</span>.<span class="name">getApplyIndexingMode</span></a></span><span class="decl_args">
10+
<span class="fn">(<span class="fn">indexMd</span> : <a href="../.././Init/MetaTypes.html#Lean.Meta.TransparencyMode">Lean.Meta.TransparencyMode</a>)</span></span>
11+
<span class="decl_args">
12+
<span class="fn">(<span class="fn">type</span> : <a href="../.././Lean/Expr.html#Lean.Expr">Lean.Expr</a>)</span></span>
13+
<span class="decl_args"> :</span><div class="decl_type"><span class="fn"><a href="../.././Lean/Meta/Basic.html#Lean.Meta.MetaM">Lean.MetaM</a> <a href="../.././Aesop/Index/Basic.html#Aesop.IndexingMode">IndexingMode</a></span></div></div><details><summary>Equations</summary><ul class="equations"><li class="equation">One or more equations did not get rendered due to their size.</li></ul></details><details id="instances-for-list-Aesop.RuleBuilder.getApplyIndexingMode" class="instances-for-list"><summary>Instances For</summary><ul class="instances-for-enum"></ul></details></div></div><div class="decl" id="Aesop.RuleBuilder.checkNoIff"><div class="def"><div class="gh_link"><a href="https://github.com/leanprover-community/aesop/blob/f0c6e183ea26531e82773feb4b73ab6595ca17a5/Aesop/Builder/Apply.lean#L36-L40">source</a></div><div class="decl_header"><span class="decl_kind">def</span>
14+
<span class="decl_name"><a class="break_within" href="../.././Aesop/Builder/Apply.html#Aesop.RuleBuilder.checkNoIff"><span class="name">Aesop</span>.<span class="name">RuleBuilder</span>.<span class="name">checkNoIff</span></a></span><span class="decl_args">
15+
<span class="fn">(<span class="fn">type</span> : <a href="../.././Lean/Expr.html#Lean.Expr">Lean.Expr</a>)</span></span>
16+
<span class="decl_args"> :</span><div class="decl_type"><span class="fn"><a href="../.././Lean/Meta/Basic.html#Lean.Meta.MetaM">Lean.MetaM</a> <a href="../.././Init/Prelude.html#Unit">Unit</a></span></div></div><details><summary>Equations</summary><ul class="equations"><li class="equation">One or more equations did not get rendered due to their size.</li></ul></details><details id="instances-for-list-Aesop.RuleBuilder.checkNoIff" class="instances-for-list"><summary>Instances For</summary><ul class="instances-for-enum"></ul></details></div></div><div class="decl" id="Aesop.RuleBuilder.applyCore"><div class="def"><div class="gh_link"><a href="https://github.com/leanprover-community/aesop/blob/f0c6e183ea26531e82773feb4b73ab6595ca17a5/Aesop/Builder/Apply.lean#L42-L49">source</a></div><div class="decl_header"><span class="decl_kind">def</span>
17+
<span class="decl_name"><a class="break_within" href="../.././Aesop/Builder/Apply.html#Aesop.RuleBuilder.applyCore"><span class="name">Aesop</span>.<span class="name">RuleBuilder</span>.<span class="name">applyCore</span></a></span><span class="decl_args">
18+
<span class="fn">(<span class="fn">t</span> : <a href="../.././Aesop/RuleTac/RuleTerm.html#Aesop.ElabRuleTerm">ElabRuleTerm</a>)</span></span>
19+
<span class="decl_args">
20+
<span class="fn">(<span class="fn">pat?</span> : <span class="fn"><a href="../.././Init/Prelude.html#Option">Option</a> <a href="../.././Aesop/RulePattern.html#Aesop.RulePattern">RulePattern</a></span>)</span></span>
21+
<span class="decl_args">
22+
<span class="fn">(<span class="fn">imode?</span> : <span class="fn"><a href="../.././Init/Prelude.html#Option">Option</a> <a href="../.././Aesop/Index/Basic.html#Aesop.IndexingMode">IndexingMode</a></span>)</span></span>
23+
<span class="decl_args">
24+
<span class="fn">(<span class="fn">md </span><span class="fn">indexMd</span> : <a href="../.././Init/MetaTypes.html#Lean.Meta.TransparencyMode">Lean.Meta.TransparencyMode</a>)</span></span>
25+
<span class="decl_args">
26+
<span class="fn">(<span class="fn">phase</span> : <a href="../.././Aesop/Builder/Basic.html#Aesop.PhaseSpec">PhaseSpec</a>)</span></span>
27+
<span class="decl_args"> :</span><div class="decl_type"><span class="fn"><a href="../.././Lean/Meta/Basic.html#Lean.Meta.MetaM">Lean.MetaM</a> <a href="../.././Aesop/RuleSet/Member.html#Aesop.LocalRuleSetMember">LocalRuleSetMember</a></span></div></div><details><summary>Equations</summary><ul class="equations"><li class="equation">One or more equations did not get rendered due to their size.</li></ul></details><details id="instances-for-list-Aesop.RuleBuilder.applyCore" class="instances-for-list"><summary>Instances For</summary><ul class="instances-for-enum"></ul></details></div></div><div class="decl" id="Aesop.RuleBuilder.apply"><div class="def"><div class="gh_link"><a href="https://github.com/leanprover-community/aesop/blob/f0c6e183ea26531e82773feb4b73ab6595ca17a5/Aesop/Builder/Apply.lean#L51-L59">source</a></div><div class="decl_header"><span class="decl_kind">def</span>
28+
<span class="decl_name"><a class="break_within" href="../.././Aesop/Builder/Apply.html#Aesop.RuleBuilder.apply"><span class="name">Aesop</span>.<span class="name">RuleBuilder</span>.<span class="name">apply</span></a></span><span class="decl_args"> :</span><div class="decl_type"><a href="../.././Aesop/Builder/Basic.html#Aesop.RuleBuilder">RuleBuilder</a></div></div><details><summary>Equations</summary><ul class="equations"><li class="equation">One or more equations did not get rendered due to their size.</li></ul></details><details id="instances-for-list-Aesop.RuleBuilder.apply" class="instances-for-list"><summary>Instances For</summary><ul class="instances-for-enum"></ul></details></div></div></main>
29+
<nav class="nav"><iframe src="../.././navbar.html" class="navframe" frameBorder="0"></iframe></nav></body></html>

0 commit comments

Comments
 (0)