<!doctype html>
<html lang="en">
<head>
<meta charset="utf-8" />
<title>Inline Code with Links</title>
</head>
<body>
<main>
<article>
<h1>Inline Code with Links</h1>
<p>
Documentation tools sometimes wrap identifiers in links inside inline code.
For example, the type <code class="hl lean inline"><a href="https://example.org/doc/ref/Nat"><span class="const token">Nat</span></a></code>
is a common type in the language.
</p>
<p>
Multiple links can appear in a single code span:
<code class="hl lean inline"><a href="https://example.org/doc/ref/List"><span class="const token">List</span></a> <a href="https://example.org/doc/ref/Nat"><span class="const token">Nat</span></a></code>
should render as <code>List Nat</code> without any markdown link syntax.
</p>
<p>
Regular links outside of code should still work normally.
See <a href="https://example.org/guide">the guide</a> for more details.
This paragraph ensures there is enough content for stable extraction.
</p>
</article>
</main>
</body>
</html>