456 lines
24 KiB
HTML
456 lines
24 KiB
HTML
<!DOCTYPE HTML>
|
|
<html lang="en" class="light sidebar-visible" dir="ltr">
|
|
<head>
|
|
<!-- Book generated using mdBook -->
|
|
<meta charset="UTF-8">
|
|
<title>Coinduction - Rust Compiler Development Guide</title>
|
|
|
|
|
|
<!-- Custom HTML head -->
|
|
|
|
<meta name="description" content="A guide to developing the Rust compiler (rustc)">
|
|
<meta name="viewport" content="width=device-width, initial-scale=1">
|
|
<meta name="theme-color" content="#ffffff">
|
|
|
|
<link rel="icon" href="../favicon.svg">
|
|
<link rel="shortcut icon" href="../favicon.png">
|
|
<link rel="stylesheet" href="../css/variables.css">
|
|
<link rel="stylesheet" href="../css/general.css">
|
|
<link rel="stylesheet" href="../css/chrome.css">
|
|
<link rel="stylesheet" href="../css/print.css" media="print">
|
|
|
|
<!-- Fonts -->
|
|
<link rel="stylesheet" href="../FontAwesome/css/font-awesome.css">
|
|
<link rel="stylesheet" href="../fonts/fonts.css">
|
|
|
|
<!-- Highlight.js Stylesheets -->
|
|
<link rel="stylesheet" id="highlight-css" href="../highlight.css">
|
|
<link rel="stylesheet" id="tomorrow-night-css" href="../tomorrow-night.css">
|
|
<link rel="stylesheet" id="ayu-highlight-css" href="../ayu-highlight.css">
|
|
|
|
<!-- Custom theme stylesheets -->
|
|
|
|
|
|
<!-- Provide site root and default themes to javascript -->
|
|
<script>
|
|
const path_to_root = "../";
|
|
const default_light_theme = "light";
|
|
const default_dark_theme = "navy";
|
|
</script>
|
|
<!-- Start loading toc.js asap -->
|
|
<script src="../toc.js"></script>
|
|
</head>
|
|
<body>
|
|
<div id="body-container">
|
|
<!-- Work around some values being stored in localStorage wrapped in quotes -->
|
|
<script>
|
|
try {
|
|
let theme = localStorage.getItem('mdbook-theme');
|
|
let sidebar = localStorage.getItem('mdbook-sidebar');
|
|
|
|
if (theme.startsWith('"') && theme.endsWith('"')) {
|
|
localStorage.setItem('mdbook-theme', theme.slice(1, theme.length - 1));
|
|
}
|
|
|
|
if (sidebar.startsWith('"') && sidebar.endsWith('"')) {
|
|
localStorage.setItem('mdbook-sidebar', sidebar.slice(1, sidebar.length - 1));
|
|
}
|
|
} catch (e) { }
|
|
</script>
|
|
|
|
<!-- Set the theme before any content is loaded, prevents flash -->
|
|
<script>
|
|
const default_theme = window.matchMedia("(prefers-color-scheme: dark)").matches ? default_dark_theme : default_light_theme;
|
|
let theme;
|
|
try { theme = localStorage.getItem('mdbook-theme'); } catch(e) { }
|
|
if (theme === null || theme === undefined) { theme = default_theme; }
|
|
const html = document.documentElement;
|
|
html.classList.remove('light')
|
|
html.classList.add(theme);
|
|
html.classList.add("js");
|
|
</script>
|
|
|
|
<input type="checkbox" id="sidebar-toggle-anchor" class="hidden">
|
|
|
|
<!-- Hide / unhide sidebar before it is displayed -->
|
|
<script>
|
|
let sidebar = null;
|
|
const sidebar_toggle = document.getElementById("sidebar-toggle-anchor");
|
|
if (document.body.clientWidth >= 1080) {
|
|
try { sidebar = localStorage.getItem('mdbook-sidebar'); } catch(e) { }
|
|
sidebar = sidebar || 'visible';
|
|
} else {
|
|
sidebar = 'hidden';
|
|
}
|
|
sidebar_toggle.checked = sidebar === 'visible';
|
|
html.classList.remove('sidebar-visible');
|
|
html.classList.add("sidebar-" + sidebar);
|
|
</script>
|
|
|
|
<nav id="sidebar" class="sidebar" aria-label="Table of contents">
|
|
<!-- populated by js -->
|
|
<mdbook-sidebar-scrollbox class="sidebar-scrollbox"></mdbook-sidebar-scrollbox>
|
|
<noscript>
|
|
<iframe class="sidebar-iframe-outer" src="../toc.html"></iframe>
|
|
</noscript>
|
|
<div id="sidebar-resize-handle" class="sidebar-resize-handle">
|
|
<div class="sidebar-resize-indicator"></div>
|
|
</div>
|
|
</nav>
|
|
|
|
<div id="page-wrapper" class="page-wrapper">
|
|
|
|
<div class="page">
|
|
<div id="menu-bar-hover-placeholder"></div>
|
|
<div id="menu-bar" class="menu-bar sticky">
|
|
<div class="left-buttons">
|
|
<label id="sidebar-toggle" class="icon-button" for="sidebar-toggle-anchor" title="Toggle Table of Contents" aria-label="Toggle Table of Contents" aria-controls="sidebar">
|
|
<i class="fa fa-bars"></i>
|
|
</label>
|
|
<button id="theme-toggle" class="icon-button" type="button" title="Change theme" aria-label="Change theme" aria-haspopup="true" aria-expanded="false" aria-controls="theme-list">
|
|
<i class="fa fa-paint-brush"></i>
|
|
</button>
|
|
<ul id="theme-list" class="theme-popup" aria-label="Themes" role="menu">
|
|
<li role="none"><button role="menuitem" class="theme" id="default_theme">Auto</button></li>
|
|
<li role="none"><button role="menuitem" class="theme" id="light">Light</button></li>
|
|
<li role="none"><button role="menuitem" class="theme" id="rust">Rust</button></li>
|
|
<li role="none"><button role="menuitem" class="theme" id="coal">Coal</button></li>
|
|
<li role="none"><button role="menuitem" class="theme" id="navy">Navy</button></li>
|
|
<li role="none"><button role="menuitem" class="theme" id="ayu">Ayu</button></li>
|
|
</ul>
|
|
<button id="search-toggle" class="icon-button" type="button" title="Search. (Shortkey: s)" aria-label="Toggle Searchbar" aria-expanded="false" aria-keyshortcuts="S" aria-controls="searchbar">
|
|
<i class="fa fa-search"></i>
|
|
</button>
|
|
</div>
|
|
|
|
<h1 class="menu-title">Rust Compiler Development Guide</h1>
|
|
|
|
<div class="right-buttons">
|
|
<a href="../print.html" title="Print this book" aria-label="Print this book">
|
|
<i id="print-button" class="fa fa-print"></i>
|
|
</a>
|
|
<a href="https://github.com/rust-lang/rustc-dev-guide" title="Git repository" aria-label="Git repository">
|
|
<i id="git-repository-button" class="fa fa-github"></i>
|
|
</a>
|
|
<a href="https://github.com/rust-lang/rustc-dev-guide/edit/master/src/solve/coinduction.md" title="Suggest an edit" aria-label="Suggest an edit">
|
|
<i id="git-edit-button" class="fa fa-edit"></i>
|
|
</a>
|
|
|
|
</div>
|
|
</div>
|
|
|
|
<div id="search-wrapper" class="hidden">
|
|
<form id="searchbar-outer" class="searchbar-outer">
|
|
<input type="search" id="searchbar" name="searchbar" placeholder="Search this book ..." aria-controls="searchresults-outer" aria-describedby="searchresults-header">
|
|
</form>
|
|
<div id="searchresults-outer" class="searchresults-outer hidden">
|
|
<div id="searchresults-header" class="searchresults-header"></div>
|
|
<ul id="searchresults">
|
|
</ul>
|
|
</div>
|
|
</div>
|
|
|
|
<!-- Apply ARIA attributes after the sidebar and the sidebar toggle button are added to the DOM -->
|
|
<script>
|
|
document.getElementById('sidebar-toggle').setAttribute('aria-expanded', sidebar === 'visible');
|
|
document.getElementById('sidebar').setAttribute('aria-hidden', sidebar !== 'visible');
|
|
Array.from(document.querySelectorAll('#sidebar a')).forEach(function(link) {
|
|
link.setAttribute('tabIndex', sidebar === 'visible' ? 0 : -1);
|
|
});
|
|
</script>
|
|
|
|
<div id="content" class="content">
|
|
<main>
|
|
<h1 id="coinduction"><a class="header" href="#coinduction">Coinduction</a></h1>
|
|
<p>The trait solver may use coinduction when proving goals.
|
|
Coinduction is fairly subtle so we're giving it its own chapter.</p>
|
|
<h2 id="coinduction-and-induction"><a class="header" href="#coinduction-and-induction">Coinduction and induction</a></h2>
|
|
<p>With induction, we recursively apply proofs until we end up with a finite proof tree.
|
|
Consider the example of <code>Vec<Vec<Vec<u32>>>: Debug</code> which results in the following tree.</p>
|
|
<ul>
|
|
<li><code>Vec<Vec<Vec<u32>>>: Debug</code>
|
|
<ul>
|
|
<li><code>Vec<Vec<u32>>: Debug</code>
|
|
<ul>
|
|
<li><code>Vec<u32>: Debug</code>
|
|
<ul>
|
|
<li><code>u32: Debug</code></li>
|
|
</ul>
|
|
</li>
|
|
</ul>
|
|
</li>
|
|
</ul>
|
|
</li>
|
|
</ul>
|
|
<p>This tree is finite. But not all goals we would want to hold have finite proof trees,
|
|
consider the following example:</p>
|
|
<pre><pre class="playground"><code class="language-rust"><span class="boring">#![allow(unused)]
|
|
</span><span class="boring">fn main() {
|
|
</span>struct List<T> {
|
|
value: T,
|
|
next: Option<Box<List<T>>>,
|
|
}
|
|
<span class="boring">}</span></code></pre></pre>
|
|
<p>For <code>List<T>: Send</code> to hold all its fields have to recursively implement <code>Send</code> as well.
|
|
This would result in the following proof tree:</p>
|
|
<ul>
|
|
<li><code>List<T>: Send</code>
|
|
<ul>
|
|
<li><code>T: Send</code></li>
|
|
<li><code>Option<Box<List<T>>>: Send</code>
|
|
<ul>
|
|
<li><code>Box<List<T>>: Send</code>
|
|
<ul>
|
|
<li><code>List<T>: Send</code>
|
|
<ul>
|
|
<li><code>T: Send</code></li>
|
|
<li><code>Option<Box<List<T>>>: Send</code>
|
|
<ul>
|
|
<li><code>Box<List<T>>: Send</code>
|
|
<ul>
|
|
<li>...</li>
|
|
</ul>
|
|
</li>
|
|
</ul>
|
|
</li>
|
|
</ul>
|
|
</li>
|
|
</ul>
|
|
</li>
|
|
</ul>
|
|
</li>
|
|
</ul>
|
|
</li>
|
|
</ul>
|
|
<p>This tree would be infinitely large which is exactly what coinduction is about.</p>
|
|
<blockquote>
|
|
<p>To <strong>inductively</strong> prove a goal you need to provide a finite proof tree for it.
|
|
To <strong>coinductively</strong> prove a goal the provided proof tree may be infinite.</p>
|
|
</blockquote>
|
|
<h2 id="why-is-coinduction-correct"><a class="header" href="#why-is-coinduction-correct">Why is coinduction correct</a></h2>
|
|
<p>When checking whether some trait goals holds, we're asking "does there exist an <code>impl</code>
|
|
which satisfies this bound". Even if are infinite chains of nested goals, we still have a
|
|
unique <code>impl</code> which should be used.</p>
|
|
<h2 id="how-to-implement-coinduction"><a class="header" href="#how-to-implement-coinduction">How to implement coinduction</a></h2>
|
|
<p>While our implementation can not check for coinduction by trying to construct an infinite
|
|
tree as that would take infinite resources, it still makes sense to think of coinduction
|
|
from this perspective.</p>
|
|
<p>As we cannot check for infinite trees, we instead search for patterns for which we know that
|
|
they would result in an infinite proof tree. The currently pattern we detect are (canonical)
|
|
cycles. If <code>T: Send</code> relies on <code>T: Send</code> then it's pretty clear that this will just go on forever.</p>
|
|
<p>With cycles we have to be careful with caching. Because of canonicalization of regions and
|
|
inference variables encountering a cycle doesn't mean that we would get an infinite proof tree.
|
|
Looking at the following example:</p>
|
|
<pre><pre class="playground"><code class="language-rust"><span class="boring">#![allow(unused)]
|
|
</span><span class="boring">fn main() {
|
|
</span>trait Foo {}
|
|
struct Wrapper<T>(T);
|
|
|
|
impl<T> Foo for Wrapper<Wrapper<T>>
|
|
where
|
|
Wrapper<T>: Foo
|
|
{}
|
|
<span class="boring">}</span></code></pre></pre>
|
|
<p>Proving <code>Wrapper<?0>: Foo</code> uses the impl <code>impl<T> Foo for Wrapper<Wrapper<T>></code> which constrains
|
|
<code>?0</code> to <code>Wrapper<?1></code> and then requires <code>Wrapper<?1>: Foo</code>. Due to canonicalization this would be
|
|
detected as a cycle.</p>
|
|
<p>The idea to solve is to return a <em>provisional result</em> whenever we detect a cycle and repeatedly
|
|
retry goals until the <em>provisional result</em> is equal to the final result of that goal. We
|
|
start out by using <code>Yes</code> with no constraints as the result and then update it to the result of
|
|
the previous iteration whenever we have to rerun.</p>
|
|
<p>TODO: elaborate here. We use the same approach as chalk for coinductive cycles.
|
|
Note that the treatment for inductive cycles currently differs by simply returning <code>Overflow</code>.
|
|
See <a href="https://rust-lang.github.io/chalk/book/recursive/inductive_cycles.html">the relevant chapters</a> in the chalk book.</p>
|
|
<h2 id="future-work"><a class="header" href="#future-work">Future work</a></h2>
|
|
<p>We currently only consider auto-traits, <code>Sized</code>, and <code>WF</code>-goals to be coinductive.
|
|
In the future we pretty much intend for all goals to be coinductive.
|
|
Lets first elaborate on why allowing more coinductive proofs is even desirable.</p>
|
|
<h3 id="recursive-data-types-already-rely-on-coinduction"><a class="header" href="#recursive-data-types-already-rely-on-coinduction">Recursive data types already rely on coinduction...</a></h3>
|
|
<p>...they just tend to avoid them in the trait solver.</p>
|
|
<pre><pre class="playground"><code class="language-rust"><span class="boring">#![allow(unused)]
|
|
</span><span class="boring">fn main() {
|
|
</span>enum List<T> {
|
|
Nil,
|
|
Succ(T, Box<List<T>>),
|
|
}
|
|
|
|
impl<T: Clone> Clone for List<T> {
|
|
fn clone(&self) -> Self {
|
|
match self {
|
|
List::Nil => List::Nil,
|
|
List::Succ(head, tail) => List::Succ(head.clone(), tail.clone()),
|
|
}
|
|
}
|
|
}
|
|
<span class="boring">}</span></code></pre></pre>
|
|
<p>We are using <code>tail.clone()</code> in this impl. For this we have to prove <code>Box<List<T>>: Clone</code>
|
|
which requires <code>List<T>: Clone</code> but that relies on the impl which we are currently checking.
|
|
By adding that requirement to the <code>where</code>-clauses of the impl, which is what we would
|
|
do with <a href="https://smallcultfollowing.com/babysteps/blog/2022/04/12/implied-bounds-and-perfect-derive">perfect derive</a>, we move that cycle into the trait solver and <a href="https://play.rust-lang.org/?version=stable&mode=debug&edition=2021&gist=0a9c3830b93a2380e6978d6328df8f72">get an error</a>.</p>
|
|
<h3 id="recursive-data-types"><a class="header" href="#recursive-data-types">Recursive data types</a></h3>
|
|
<p>We also need coinduction to reason about recursive types containing projections,
|
|
e.g. the following currently fails to compile even though it should be valid.</p>
|
|
<pre><pre class="playground"><code class="language-rust"><span class="boring">#![allow(unused)]
|
|
</span><span class="boring">fn main() {
|
|
</span>use std::borrow::Cow;
|
|
pub struct Foo<'a>(Cow<'a, [Foo<'a>]>);
|
|
<span class="boring">}</span></code></pre></pre>
|
|
<p>This issue has been known since at least 2015, see
|
|
<a href="https://github.com/rust-lang/rust/issues/23714">#23714</a> if you want to know more.</p>
|
|
<h3 id="explicitly-checked-implied-bounds"><a class="header" href="#explicitly-checked-implied-bounds">Explicitly checked implied bounds</a></h3>
|
|
<p>When checking an impl, we assume that the types in the impl headers are well-formed.
|
|
This means that when using instantiating the impl we have to prove that's actually the case.
|
|
<a href="https://github.com/rust-lang/rust/issues/100051">#100051</a> shows that this is not the case.
|
|
To fix this, we have to add <code>WF</code> predicates for the types in impl headers.
|
|
Without coinduction for all traits, this even breaks <code>core</code>.</p>
|
|
<pre><pre class="playground"><code class="language-rust"><span class="boring">#![allow(unused)]
|
|
</span><span class="boring">fn main() {
|
|
</span>trait FromResidual<R> {}
|
|
trait Try: FromResidual<<Self as Try>::Residual> {
|
|
type Residual;
|
|
}
|
|
|
|
struct Ready<T>(T);
|
|
impl<T> Try for Ready<T> {
|
|
type Residual = Ready<()>;
|
|
}
|
|
impl<T> FromResidual<<Ready<T> as Try>::Residual> for Ready<T> {}
|
|
<span class="boring">}</span></code></pre></pre>
|
|
<p>When checking that the impl of <code>FromResidual</code> is well formed we get the following cycle:</p>
|
|
<p>The impl is well formed if <code><Ready<T> as Try>::Residual</code> and <code>Ready<T></code> are well formed.</p>
|
|
<ul>
|
|
<li><code>wf(<Ready<T> as Try>::Residual)</code> requires</li>
|
|
<li><code>Ready<T>: Try</code>, which requires because of the super trait</li>
|
|
<li><code>Ready<T>: FromResidual<Ready<T> as Try>::Residual></code>, <strong>because of implied bounds on impl</strong></li>
|
|
<li><code>wf(<Ready<T> as Try>::Residual)</code> :tada: <strong>cycle</strong></li>
|
|
</ul>
|
|
<h3 id="issues-when-extending-coinduction-to-more-goals"><a class="header" href="#issues-when-extending-coinduction-to-more-goals">Issues when extending coinduction to more goals</a></h3>
|
|
<p>There are some additional issues to keep in mind when extending coinduction.
|
|
The issues here are not relevant for the current solver.</p>
|
|
<h4 id="implied-super-trait-bounds"><a class="header" href="#implied-super-trait-bounds">Implied super trait bounds</a></h4>
|
|
<p>Our trait system currently treats super traits, e.g. <code>trait Trait: SuperTrait</code>,
|
|
by 1) requiring that <code>SuperTrait</code> has to hold for all types which implement <code>Trait</code>,
|
|
and 2) assuming <code>SuperTrait</code> holds if <code>Trait</code> holds.</p>
|
|
<p>Relying on 2) while proving 1) is unsound. This can only be observed in case of
|
|
coinductive cycles. Without cycles, whenever we rely on 2) we must have also
|
|
proven 1) without relying on 2) for the used impl of <code>Trait</code>.</p>
|
|
<pre><pre class="playground"><code class="language-rust"><span class="boring">#![allow(unused)]
|
|
</span><span class="boring">fn main() {
|
|
</span>trait Trait: SuperTrait {}
|
|
|
|
impl<T: Trait> Trait for T {}
|
|
|
|
// Keeping the current setup for coinduction
|
|
// would allow this compile. Uff :<
|
|
fn sup<T: SuperTrait>() {}
|
|
fn requires_trait<T: Trait>() { sup::<T>() }
|
|
fn generic<T>() { requires_trait::<T>() }
|
|
<span class="boring">}</span></code></pre></pre>
|
|
<p>This is not really fundamental to coinduction but rather an existing property
|
|
which is made unsound because of it.</p>
|
|
<h5 id="possible-solutions"><a class="header" href="#possible-solutions">Possible solutions</a></h5>
|
|
<p>The easiest way to solve this would be to completely remove 2) and always elaborate
|
|
<code>T: Trait</code> to <code>T: Trait</code> and <code>T: SuperTrait</code> outside of the trait solver.
|
|
This would allow us to also remove 1), but as we still have to prove ordinary
|
|
<code>where</code>-bounds on traits, that's just additional work.</p>
|
|
<p>While one could imagine ways to disable cyclic uses of 2) when checking 1),
|
|
at least the ideas of myself - @lcnr - are all far to complex to be reasonable.</p>
|
|
<h4 id="normalizes_to-goals-and-progress"><a class="header" href="#normalizes_to-goals-and-progress"><code>normalizes_to</code> goals and progress</a></h4>
|
|
<p>A <code>normalizes_to</code> goal represents the requirement that <code><T as Trait>::Assoc</code> normalizes
|
|
to some <code>U</code>. This is achieved by defacto first normalizing <code><T as Trait>::Assoc</code> and then
|
|
equating the resulting type with <code>U</code>. It should be a mapping as each projection should normalize
|
|
to exactly one type. By simply allowing infinite proof trees, we would get the following behavior:</p>
|
|
<pre><pre class="playground"><code class="language-rust"><span class="boring">#![allow(unused)]
|
|
</span><span class="boring">fn main() {
|
|
</span>trait Trait {
|
|
type Assoc;
|
|
}
|
|
|
|
impl Trait for () {
|
|
type Assoc = <() as Trait>::Assoc;
|
|
}
|
|
<span class="boring">}</span></code></pre></pre>
|
|
<p>If we now compute <code>normalizes_to(<() as Trait>::Assoc, Vec<u32>)</code>, we would resolve the impl
|
|
and get the associated type <code><() as Trait>::Assoc</code>. We then equate that with the expected type,
|
|
causing us to check <code>normalizes_to(<() as Trait>::Assoc, Vec<u32>)</code> again.
|
|
This just goes on forever, resulting in an infinite proof tree.</p>
|
|
<p>This means that <code><() as Trait>::Assoc</code> would be equal to any other type which is unsound.</p>
|
|
<h5 id="how-to-solve-this"><a class="header" href="#how-to-solve-this">How to solve this</a></h5>
|
|
<p><strong>WARNING: THIS IS SUBTLE AND MIGHT BE WRONG</strong></p>
|
|
<p>Unlike trait goals, <code>normalizes_to</code> has to be <em>productive</em><sup class="footnote-reference" id="fr-1-1"><a href="#footnote-1">1</a></sup>. A <code>normalizes_to</code> goal
|
|
is productive once the projection normalizes to a rigid type constructor,
|
|
so <code><() as Trait>::Assoc</code> normalizing to <code>Vec<<() as Trait>::Assoc></code> would be productive.</p>
|
|
<p>A <code>normalizes_to</code> goal has two kinds of nested goals. Nested requirements needed to actually
|
|
normalize the projection, and the equality between the normalized projection and the
|
|
expected type. Only the equality has to be productive. A branch in the proof tree is productive
|
|
if it is either finite, or contains at least one <code>normalizes_to</code> where the alias is resolved
|
|
to a rigid type constructor.</p>
|
|
<p>Alternatively, we could simply always treat the equate branch of <code>normalizes_to</code> as inductive.
|
|
Any cycles should result in infinite types, which aren't supported anyways and would only
|
|
result in overflow when deeply normalizing for codegen.</p>
|
|
<p>experimentation and examples: <a href="https://hackmd.io/-8p0AHnzSq2VAE6HE_wX-w?view">https://hackmd.io/-8p0AHnzSq2VAE6HE_wX-w?view</a></p>
|
|
<p>Another attempt at a summary.</p>
|
|
<ul>
|
|
<li>in projection eq, we must make progress with constraining the rhs</li>
|
|
<li>a cycle is only ok if while equating we have a rigid ty on the lhs after norm at least once</li>
|
|
<li>cycles outside of the recursive <code>eq</code> call of <code>normalizes_to</code> are always fine</li>
|
|
</ul>
|
|
<hr>
|
|
<ol class="footnote-definition"><li id="footnote-1">
|
|
<p>related: <a href="https://coq.inria.fr/refman/language/core/coinductive.html#top-level-definitions-of-corecursive-functions">https://coq.inria.fr/refman/language/core/coinductive.html#top-level-definitions-of-corecursive-functions</a> <a href="#fr-1-1">↩</a></p>
|
|
</li>
|
|
</ol>
|
|
</main>
|
|
|
|
<nav class="nav-wrapper" aria-label="Page navigation">
|
|
<!-- Mobile navigation buttons -->
|
|
<a rel="prev" href="../solve/canonicalization.html" class="mobile-nav-chapters previous" title="Previous chapter" aria-label="Previous chapter" aria-keyshortcuts="Left">
|
|
<i class="fa fa-angle-left"></i>
|
|
</a>
|
|
|
|
<a rel="next prefetch" href="../solve/caching.html" class="mobile-nav-chapters next" title="Next chapter" aria-label="Next chapter" aria-keyshortcuts="Right">
|
|
<i class="fa fa-angle-right"></i>
|
|
</a>
|
|
|
|
<div style="clear: both"></div>
|
|
</nav>
|
|
</div>
|
|
</div>
|
|
|
|
<nav class="nav-wide-wrapper" aria-label="Page navigation">
|
|
<a rel="prev" href="../solve/canonicalization.html" class="nav-chapters previous" title="Previous chapter" aria-label="Previous chapter" aria-keyshortcuts="Left">
|
|
<i class="fa fa-angle-left"></i>
|
|
</a>
|
|
|
|
<a rel="next prefetch" href="../solve/caching.html" class="nav-chapters next" title="Next chapter" aria-label="Next chapter" aria-keyshortcuts="Right">
|
|
<i class="fa fa-angle-right"></i>
|
|
</a>
|
|
</nav>
|
|
|
|
</div>
|
|
|
|
|
|
|
|
|
|
<script>
|
|
window.playground_copyable = true;
|
|
</script>
|
|
|
|
|
|
<script src="../elasticlunr.min.js"></script>
|
|
<script src="../mark.min.js"></script>
|
|
<script src="../searcher.js"></script>
|
|
|
|
<script src="../clipboard.min.js"></script>
|
|
<script src="../highlight.js"></script>
|
|
<script src="../book.js"></script>
|
|
|
|
<!-- Custom JS scripts -->
|
|
<script src="../mermaid.min.js"></script>
|
|
<script src="../mermaid-init.js"></script>
|
|
|
|
|
|
</div>
|
|
</body>
|
|
</html>
|