531 lines
21 KiB
HTML
531 lines
21 KiB
HTML
<!DOCTYPE html>
|
||
<html lang="en"><head>
|
||
<meta charset="utf-8">
|
||
<meta http-equiv="X-UA-Compatible" content="IE=edge">
|
||
<meta name="viewport" content="width=device-width, initial-scale=1">
|
||
<title>Style guide for PLFA | Programming Language Foundations in Agda
|
||
</title><!-- Begin Jekyll SEO tag v2.6.1 -->
|
||
<meta name="generator" content="Jekyll v3.9.0" />
|
||
<meta property="og:title" content="Style guide for PLFA" />
|
||
<meta property="og:locale" content="en_US" />
|
||
<meta name="description" content="Programming Language Foundations in Agda" />
|
||
<meta property="og:description" content="Programming Language Foundations in Agda" />
|
||
<link rel="canonical" href="https://plfa.github.io/20.07/style-guide.html" />
|
||
<meta property="og:url" content="https://plfa.github.io/20.07/style-guide.html" />
|
||
<meta property="og:site_name" content="Programming Language Foundations in Agda" />
|
||
<script type="application/ld+json">
|
||
{"url":"https://plfa.github.io/20.07/style-guide.html","headline":"Style guide for PLFA","description":"Programming Language Foundations in Agda","@type":"WebPage","@context":"https://schema.org"}</script>
|
||
<!-- End Jekyll SEO tag -->
|
||
<link rel="stylesheet" href="/20.07/assets/main.css"></head>
|
||
<body><header class="site-header" role="banner">
|
||
|
||
<div class="wrapper">
|
||
|
||
<a class="site-title" href="/20.07/">Programming Language Foundations in Agda
|
||
</a>
|
||
|
||
<nav class="site-nav">
|
||
<span class="menu-icon">
|
||
<svg viewBox="0 0 18 15" width="18px" height="15px">
|
||
<path fill="#424242" d="M18,1.484c0,0.82-0.665,1.484-1.484,1.484H1.484C0.665,2.969,0,2.304,0,1.484l0,0C0,0.665,0.665,0,1.484,0 h15.031C17.335,0,18,0.665,18,1.484L18,1.484z"/>
|
||
<path fill="#424242" d="M18,7.516C18,8.335,17.335,9,16.516,9H1.484C0.665,9,0,8.335,0,7.516l0,0c0-0.82,0.665-1.484,1.484-1.484 h15.031C17.335,6.031,18,6.696,18,7.516L18,7.516z"/>
|
||
<path fill="#424242" d="M18,13.516C18,14.335,17.335,15,16.516,15H1.484C0.665,15,0,14.335,0,13.516l0,0 c0-0.82,0.665-1.484,1.484-1.484h15.031C17.335,12.031,18,12.696,18,13.516L18,13.516z"/>
|
||
</svg>
|
||
</span>
|
||
|
||
<div class="trigger">
|
||
<a class="page-link" href="/20.07/">The Book</a>
|
||
<a class="page-link" href="/20.07/Announcements/">Announcements</a>
|
||
<a class="page-link" href="/20.07/GettingStarted/">Getting Started</a>
|
||
<a class="page-link" href="/20.07/Citing/">Citing</a>
|
||
<a class="page-link" href="https://agda-zh.github.io/PLFA-zh/">中文</a>
|
||
</div>
|
||
</nav>
|
||
|
||
</div>
|
||
|
||
</header>
|
||
<main class="page-content" aria-label="Content">
|
||
<div class="wrapper">
|
||
<article class="post">
|
||
|
||
<header class="post-header">
|
||
<h1 class="post-title">Style guide for PLFA</h1>
|
||
</header>
|
||
|
||
<p style="text-align:center;">
|
||
|
||
|
||
|
||
|
||
|
||
</p>
|
||
|
||
|
||
<div class="post-content">
|
||
<h1 id="style-guide-for-plfa">Style guide for PLFA</h1>
|
||
|
||
<p>This is based on <a href="https://github.com/agda/agda-stdlib/blob/master/notes/style-guide.md">the style guide for the Agda standard library</a>.
|
||
Like it, this is very much a work-in-progress and is not exhaustive.</p>
|
||
|
||
<h2 id="file-structure">File structure</h2>
|
||
|
||
<h4 id="module-imports">Module imports</h4>
|
||
|
||
<ul>
|
||
<li>
|
||
<p>All module imports should be placed at the top of the file immediately
|
||
after the module declaration.</p>
|
||
</li>
|
||
<li>
|
||
<p>If the module takes parameters that require imports from other files
|
||
then those imports only may be placed above the module declaration.</p>
|
||
</li>
|
||
<li>If it is important that certain names only come into scope later in
|
||
the file then the module should still be imported at the top of the
|
||
file but it can be given a shorter name using <code class="language-plaintext highlighter-rouge">as</code> and then opened
|
||
later on in the file when needed, e.g.
|
||
<pre><code class="language-agda">import Data.List.Relation.Binary.Equality.Setoid as SetoidEquality
|
||
...
|
||
...
|
||
open SetoidEquality S
|
||
</code></pre>
|
||
</li>
|
||
<li>
|
||
<p>The list of module imports should be in alphabetical order.</p>
|
||
</li>
|
||
<li>When using only a few items from a module, the items should be
|
||
enumerated in the import with <code class="language-plaintext highlighter-rouge">using</code> in order to make dependencies
|
||
clearer.</li>
|
||
</ul>
|
||
|
||
<h4 id="indentation">Indentation</h4>
|
||
|
||
<ul>
|
||
<li>
|
||
<p>The contents of a top-level module should have zero indentation.</p>
|
||
</li>
|
||
<li>
|
||
<p>Every subsequent nested scope should then be indented by an additional
|
||
two spaces.</p>
|
||
</li>
|
||
<li>
|
||
<p><code class="language-plaintext highlighter-rouge">where</code> blocks should be indented by two spaces and their contents
|
||
should be aligned with the <code class="language-plaintext highlighter-rouge">where</code>.</p>
|
||
</li>
|
||
<li>If the type of a term does not fit on one line then the subsequent
|
||
lines of the type should all be indented by two spaces, e.g.
|
||
<pre><code class="language-agda">map-cong₂ : ∀ {a b} {A : Set a} {B : Set b}
|
||
→ ∀ {f g : A → B} {xs}
|
||
→ All (λ x → f x ≡ g x) xs → map f xs ≡ map g xs
|
||
</code></pre>
|
||
</li>
|
||
<li>As can be seen in the example above, function arrows at line breaks
|
||
should always go at the beginning of the next line rather than the
|
||
end of the line.</li>
|
||
</ul>
|
||
|
||
<h4 id="module-parameters">Module parameters</h4>
|
||
|
||
<ul>
|
||
<li>
|
||
<p>Module parameters should be put on a single line if they fit.</p>
|
||
</li>
|
||
<li>
|
||
<p>If they don’t fit on a single line, then they should be spread out
|
||
over multiple lines, each indented by two spaces. If they can be
|
||
grouped logically by line then it is fine to do so, otherwise a line
|
||
each is probably clearest.</p>
|
||
</li>
|
||
<li>
|
||
<p>The <code class="language-plaintext highlighter-rouge">where</code> should go on it’s own line at the end.</p>
|
||
</li>
|
||
<li>
|
||
<p>For example:</p>
|
||
<pre><code class="language-agda">module Relation.Binary.Reasoning.Base.Single
|
||
{a ℓ} {A : Set a} (_∼_ : Rel A ℓ)
|
||
(refl : Reflexive _∼_) (trans : Transitive _∼_)
|
||
where
|
||
</code></pre>
|
||
</li>
|
||
</ul>
|
||
|
||
<h4 id="reasoning-layout">Reasoning layout</h4>
|
||
|
||
<ul>
|
||
<li>
|
||
<p>The <code class="language-plaintext highlighter-rouge">begin</code> clause should go on a new line.</p>
|
||
</li>
|
||
<li>
|
||
<p>Every subsequent combinator <code class="language-plaintext highlighter-rouge">_≡⟨_⟩_</code> should go on its own line,
|
||
with the intermediate terms on their own line, indented by two spaces.</p>
|
||
</li>
|
||
<li>
|
||
<p>The relation sign (e.g. <code class="language-plaintext highlighter-rouge">≡</code>) for each line should be aligned if possible.</p>
|
||
</li>
|
||
<li>For example:
|
||
<pre><code class="language-agda">+-comm : Commutative _+_
|
||
+-comm zero n = sym (+-identityʳ n)
|
||
+-comm (suc m) n =
|
||
begin
|
||
suc m + n
|
||
≡⟨⟩
|
||
suc (m + n)
|
||
≡⟨ cong suc (+-comm m n) ⟩
|
||
suc (n + m)
|
||
≡⟨ sym (+-suc n m) ⟩
|
||
n + suc m
|
||
∎
|
||
</code></pre>
|
||
</li>
|
||
<li>When multiple reasoning frameworks need to be used in the same file, the
|
||
<code class="language-plaintext highlighter-rouge">open</code> statement should always come in a where clause local to the
|
||
definition. This way users can easily see which reasoning toolkit is
|
||
being used. For instance:
|
||
<pre><code class="language-agda">foo m n p = begin
|
||
(...) ∎
|
||
where open ≤-Reasoning
|
||
</code></pre>
|
||
</li>
|
||
</ul>
|
||
|
||
<h4 id="record-layout">Record layout</h4>
|
||
|
||
<ul>
|
||
<li>
|
||
<p>The <code class="language-plaintext highlighter-rouge">record</code> declaration should go on the same line as the rest of the proof.</p>
|
||
</li>
|
||
<li>
|
||
<p>The next line with the first record item should start with a single <code class="language-plaintext highlighter-rouge">{</code>.</p>
|
||
</li>
|
||
<li>
|
||
<p>Every subsequent item of the record should go on its own line starting with
|
||
a <code class="language-plaintext highlighter-rouge">;</code>.</p>
|
||
</li>
|
||
<li>
|
||
<p>The final line should end with <code class="language-plaintext highlighter-rouge">}</code> on its own.</p>
|
||
</li>
|
||
<li>
|
||
<p>For example:</p>
|
||
<pre><code class="language-agda">≤-isPreorder : IsPreorder _≡_ _≤_
|
||
≤-isPreorder = record
|
||
{ isEquivalence = isEquivalence
|
||
; reflexive = ≤-reflexive
|
||
; trans = ≤-trans
|
||
}
|
||
</code></pre>
|
||
</li>
|
||
</ul>
|
||
|
||
<h4 id="where-blocks"><code class="language-plaintext highlighter-rouge">where</code> blocks</h4>
|
||
|
||
<ul>
|
||
<li>
|
||
<p><code class="language-plaintext highlighter-rouge">where</code> blocks are preferred rather than the <code class="language-plaintext highlighter-rouge">let</code> construction.</p>
|
||
</li>
|
||
<li>
|
||
<p>The <code class="language-plaintext highlighter-rouge">where</code> should be placed on the line below the main proof,
|
||
indented by two spaces.</p>
|
||
</li>
|
||
<li>If the contents of the block is non-trivial then types should be
|
||
provided alongside the terms, and all terms should be on lines after
|
||
the <code class="language-plaintext highlighter-rouge">where</code>, e.g.
|
||
<pre><code class="language-agda">statement : Statement
|
||
statement = proof
|
||
where
|
||
proof : Proof
|
||
proof = some-very-long-proof
|
||
</code></pre>
|
||
</li>
|
||
<li>If the contents of the block is trivial or is an <code class="language-plaintext highlighter-rouge">open</code> statement then
|
||
it can provided on the same line as the <code class="language-plaintext highlighter-rouge">where</code> and a type can be
|
||
omitted, e.g.
|
||
<pre><code class="language-agda">statement : Statement
|
||
statement = proof
|
||
where proof = x
|
||
</code></pre>
|
||
</li>
|
||
</ul>
|
||
|
||
<h4 id="other">Other</h4>
|
||
|
||
<ul>
|
||
<li>
|
||
<p>Non-trivial proofs in <code class="language-plaintext highlighter-rouge">private</code> blocks are generally discouraged. If its
|
||
non-trivial then the chances are someone will want to reuse it as some
|
||
point!</p>
|
||
</li>
|
||
<li>
|
||
<p>The <code class="language-plaintext highlighter-rouge">with</code> syntax is preferred over the use of <code class="language-plaintext highlighter-rouge">case</code> from the <code class="language-plaintext highlighter-rouge">Function</code>
|
||
module.</p>
|
||
</li>
|
||
</ul>
|
||
|
||
<h2 id="types">Types</h2>
|
||
|
||
<h4 id="implicit-and-explicit-arguments">Implicit and explicit arguments</h4>
|
||
|
||
<ul>
|
||
<li>
|
||
<p>Functions arguments should be implicit if they can “almost always”
|
||
be inferred. If there are common cases where they cannot be inferred
|
||
then they should be left explicit.</p>
|
||
</li>
|
||
<li>
|
||
<p>If there are lots of implicit arguments that are common to a collection
|
||
of proofs they should be extracted by using an anonymous module.</p>
|
||
</li>
|
||
<li>
|
||
<p>Implicit of type <code class="language-plaintext highlighter-rouge">Level</code> and <code class="language-plaintext highlighter-rouge">Set</code> can be generalised using <code class="language-plaintext highlighter-rouge">variable</code>.
|
||
At the moment the policy is <em>not</em> to generalise over any other types in
|
||
order to minimise the amount of information that users have to keep in
|
||
their head concurrently.</p>
|
||
</li>
|
||
</ul>
|
||
|
||
<h2 id="naming-conventions">Naming conventions</h2>
|
||
|
||
<ul>
|
||
<li>
|
||
<p>Names should be descriptive - i.e. given the name of a proof and the
|
||
module it lives in then users should be able to make a reasonable
|
||
guess at what it contains.</p>
|
||
</li>
|
||
<li>
|
||
<p>Terms from other modules should only be renamed to avoid name clashes,
|
||
otherwise all names should be used as defined.</p>
|
||
</li>
|
||
<li>
|
||
<p>Datatype names should be capitalised and function names should be
|
||
lowercase.</p>
|
||
</li>
|
||
</ul>
|
||
|
||
<h4 id="variables">Variables</h4>
|
||
|
||
<ul>
|
||
<li>
|
||
<p>Natural variables are named <code class="language-plaintext highlighter-rouge">m</code>, <code class="language-plaintext highlighter-rouge">n</code>, <code class="language-plaintext highlighter-rouge">o</code>, … (default <code class="language-plaintext highlighter-rouge">n</code>)</p>
|
||
</li>
|
||
<li>
|
||
<p>Integer variables are named <code class="language-plaintext highlighter-rouge">i</code>, <code class="language-plaintext highlighter-rouge">j</code>, <code class="language-plaintext highlighter-rouge">k</code>, … (default <code class="language-plaintext highlighter-rouge">i</code>)</p>
|
||
</li>
|
||
<li>
|
||
<p>Rational variables are named <code class="language-plaintext highlighter-rouge">p</code>, <code class="language-plaintext highlighter-rouge">q</code>, <code class="language-plaintext highlighter-rouge">r</code>, … (default <code class="language-plaintext highlighter-rouge">p</code>)</p>
|
||
</li>
|
||
<li>
|
||
<p>When naming proofs, the variables should occur in order, e.g.
|
||
<code class="language-plaintext highlighter-rouge">m≤n+m</code> rather than <code class="language-plaintext highlighter-rouge">n≤m+n</code>.</p>
|
||
</li>
|
||
<li>
|
||
<p>Collections of elements are usually indicated by appending an <code class="language-plaintext highlighter-rouge">s</code>
|
||
(e.g. if you are naming your variables <code class="language-plaintext highlighter-rouge">x</code> and <code class="language-plaintext highlighter-rouge">y</code> then lists
|
||
should be named <code class="language-plaintext highlighter-rouge">xs</code> and <code class="language-plaintext highlighter-rouge">ys</code>).</p>
|
||
</li>
|
||
</ul>
|
||
|
||
<h4 id="preconditions-and-postconditions">Preconditions and postconditions</h4>
|
||
|
||
<ul>
|
||
<li>
|
||
<p>Preconditions should only be included in names of results if
|
||
“important” (mostly judgement call).</p>
|
||
</li>
|
||
<li>
|
||
<p>Preconditions of results should be prepended to a description
|
||
of the result by using the symbol <code class="language-plaintext highlighter-rouge">⇒</code> in names (e.g. <code class="language-plaintext highlighter-rouge">asym⇒antisym</code>)</p>
|
||
</li>
|
||
<li>
|
||
<p>Preconditions and postconditions should be combined using the symbols
|
||
<code class="language-plaintext highlighter-rouge">∨</code> and <code class="language-plaintext highlighter-rouge">∧</code> (e.g. <code class="language-plaintext highlighter-rouge">m*n≡0⇒m≡0∨n≡0</code>)</p>
|
||
</li>
|
||
<li>
|
||
<p>Try to avoid the need for bracketing but if necessary use square
|
||
brackets (e.g. <code class="language-plaintext highlighter-rouge">[m∸n]⊓[n∸m]≡0</code>)</p>
|
||
</li>
|
||
</ul>
|
||
|
||
<h4 id="operators-and-relations">Operators and relations</h4>
|
||
|
||
<ul>
|
||
<li>
|
||
<p>Operators and relations should be defined using mixfix notation where
|
||
applicable (e.g. <code class="language-plaintext highlighter-rouge">_+_</code>, <code class="language-plaintext highlighter-rouge">_<_</code>)</p>
|
||
</li>
|
||
<li>
|
||
<p>Common properties such as those in rings/orders/equivalences etc.
|
||
have defined abbreviations (e.g. commutativity is shortened to <code class="language-plaintext highlighter-rouge">comm</code>).
|
||
<code class="language-plaintext highlighter-rouge">Data.Nat.Properties</code> is a good place to look for examples.</p>
|
||
</li>
|
||
<li>
|
||
<p>Properties should be by prefixed by the relevant operator/relation
|
||
(e.g. commutativity of <code class="language-plaintext highlighter-rouge">_+_</code> is named <code class="language-plaintext highlighter-rouge">+-comm</code>)</p>
|
||
</li>
|
||
<li>
|
||
<p>If the relevant unicode characters are available, negated forms of
|
||
relations should be used over the <code class="language-plaintext highlighter-rouge">¬</code> symbol (e.g. <code class="language-plaintext highlighter-rouge">m+n≮n</code> should be
|
||
used instead of <code class="language-plaintext highlighter-rouge">¬m+n<n</code>).</p>
|
||
</li>
|
||
</ul>
|
||
|
||
<h4 id="functions-and-relations-over-specific-datatypes">Functions and relations over specific datatypes</h4>
|
||
|
||
<ul>
|
||
<li>When defining a new relation over a datatype
|
||
(e.g. <code class="language-plaintext highlighter-rouge">Data.List.Relation.Binary.Pointwise</code>)
|
||
it is often common to define how to introduce and eliminate that
|
||
relation over various simple functions (e.g. <code class="language-plaintext highlighter-rouge">map</code>) over that datatype:
|
||
<pre><code class="language-agda">map⁺ : Pointwise (λ a b → R (f a) (g b)) as bs →
|
||
Pointwise R (map f as) (map g bs)
|
||
|
||
map⁻ : Pointwise R (map f as) (map g bs) →
|
||
Pointwise (λ a b → R (f a) (g b)) as bs
|
||
</code></pre>
|
||
<p>Such elimination and introduction proofs are called the name of the
|
||
function superscripted with either a <code class="language-plaintext highlighter-rouge">+</code> or <code class="language-plaintext highlighter-rouge">-</code> accordingly.</p>
|
||
</li>
|
||
</ul>
|
||
|
||
</div>
|
||
|
||
<p style="text-align:center;">
|
||
|
||
|
||
|
||
|
||
|
||
</p>
|
||
|
||
|
||
</article>
|
||
|
||
</div>
|
||
</main><footer class="site-footer h-card">
|
||
<data class="u-url" href="/20.07/"></data>
|
||
|
||
<div class="wrapper">
|
||
|
||
<h2 class="footer-heading">Programming Language Foundations in Agda
|
||
</h2><div class="footer-col-wrapper">
|
||
<div class="footer-col footer-col-1">
|
||
<ul class="contact-list">
|
||
<li class="p-name">Philip Wadler</li>
|
||
<li><a class="u-email" href="mailto:wadler@inf.ed.ac.uk">wadler@inf.ed.ac.uk</a></li>
|
||
</ul>
|
||
</div>
|
||
|
||
<div class="footer-col footer-col-2"><ul class="social-media-list"><li><a href="https://github.com/wadler"><svg class="svg-icon"><use xlink:href="/20.07/assets/minima-social-icons.svg#github"></use></svg> <span class="username">wadler</span></a></li></ul>
|
||
</div>
|
||
|
||
<div class="footer-col footer-col-3"></div>
|
||
</div><div class="footer-col-wrapper">
|
||
<div class="footer-col footer-col-1">
|
||
<ul class="contact-list">
|
||
<li class="p-name">Wen Kokke</li>
|
||
<li><a class="u-email" href="mailto:wen.kokke@ed.ac.uk">wen.kokke@ed.ac.uk</a></li>
|
||
</ul>
|
||
</div>
|
||
|
||
<div class="footer-col footer-col-2"><ul class="social-media-list"><li><a href="https://github.com/wenkokke"><svg class="svg-icon"><use xlink:href="/20.07/assets/minima-social-icons.svg#github"></use></svg> <span class="username">wenkokke</span></a></li><li><a href="https://www.twitter.com/wenkokke"><svg class="svg-icon"><use xlink:href="/20.07/assets/minima-social-icons.svg#twitter"></use></svg> <span class="username">wenkokke</span></a></li></ul>
|
||
</div>
|
||
|
||
<div class="footer-col footer-col-3"></div>
|
||
</div><div class="footer-col-wrapper">
|
||
<div class="footer-col footer-col-1">
|
||
<ul class="contact-list">
|
||
<li class="p-name">Jeremy G. Siek</li>
|
||
<li><a class="u-email" href="mailto:jsiek@indiana.edu">jsiek@indiana.edu</a></li>
|
||
</ul>
|
||
</div>
|
||
|
||
<div class="footer-col footer-col-2"><ul class="social-media-list"><li><a href="https://github.com/jsiek"><svg class="svg-icon"><use xlink:href="/20.07/assets/minima-social-icons.svg#github"></use></svg> <span class="username">jsiek</span></a></li><li><a href="https://www.twitter.com/jeremysiek"><svg class="svg-icon"><use xlink:href="/20.07/assets/minima-social-icons.svg#twitter"></use></svg> <span class="username">jeremysiek</span></a></li></ul>
|
||
</div>
|
||
|
||
<div class="footer-col footer-col-3"></div>
|
||
</div>This work is licensed under a <a rel="license" href="https://creativecommons.org/licenses/by/4.0/">Creative Commons Attribution 4.0 International License</a>
|
||
</div>
|
||
</footer>
|
||
<!-- Import jQuery -->
|
||
<script type="text/javascript" src="/20.07/assets/jquery.js"></script>
|
||
|
||
<script src="https://cdnjs.cloudflare.com/ajax/libs/anchor-js/4.2.2/anchor.min.js" integrity="sha256-E4RlfxwyJVmkkk0szw7LYJxuPlp6evtPSBDlWHsYYL8=" crossorigin="anonymous"></script>
|
||
<script type="text/javascript">
|
||
anchors.add();
|
||
</script>
|
||
|
||
<script type="text/javascript">
|
||
|
||
// Makes sandwhich menu works
|
||
$('.menu-icon').click(function(){
|
||
$('.trigger').toggle();
|
||
});
|
||
|
||
// Script which allows for foldable code blocks
|
||
$('div.foldable pre').each(function(){
|
||
var autoHeight = $(this).height();
|
||
var lineHeight = parseFloat($(this).css('line-height'));
|
||
|
||
var plus = $("<div></div>");
|
||
var horLine = $("<div></div>");
|
||
var verLine = $("<div></div>");
|
||
$(this).prepend(plus);
|
||
plus.css({
|
||
'position' : 'relative',
|
||
'float' : 'right',
|
||
'right' : '-' + (0.5 * lineHeight - 1.5) + 'px',
|
||
'width' : lineHeight,
|
||
'height' : lineHeight});
|
||
verLine.css({
|
||
'position' : 'relative',
|
||
'height' : lineHeight,
|
||
'width' : '3px',
|
||
'background-color' : '#C1E0FF'});
|
||
horLine.css({
|
||
'position' : 'relative',
|
||
'top' : '-' + (0.5 * lineHeight + 1.5) + 'px',
|
||
'left' : '-' + (0.5 * lineHeight - 1.5) + 'px',
|
||
'height' : '3px',
|
||
'width' : lineHeight,
|
||
'background-color' : '#C1E0FF'});
|
||
plus.append(verLine);
|
||
plus.append(horLine);
|
||
|
||
$(this).height(2.0 * lineHeight);
|
||
$(this).css('overflow','hidden');
|
||
|
||
$(this).click(function(){
|
||
if ($(this).height() == autoHeight) {
|
||
$(this).height(2.0 * lineHeight);
|
||
plus.show();
|
||
}
|
||
else {
|
||
$(this).height('auto');
|
||
plus.hide();
|
||
}
|
||
});
|
||
});
|
||
</script>
|
||
|
||
<!-- Import KaTeX -->
|
||
<script type="text/javascript" src="/20.07/assets/katex.js"></script>
|
||
|
||
<!-- Script which renders TeX using KaTeX -->
|
||
<script type="text/javascript">
|
||
$("script[type='math/tex']").replaceWith(
|
||
function(){
|
||
var tex = $(this).text();
|
||
return "<span class=\"inline-equation\">" +
|
||
katex.renderToString(tex) +
|
||
"</span>";
|
||
});
|
||
$("script[type='math/tex; mode=display']").replaceWith(
|
||
function(){
|
||
var tex = $(this).text().replace(/%.*?(\n|$)/g,"");
|
||
return "<div class=\"equation\">" +
|
||
katex.renderToString("\\displaystyle "+tex) +
|
||
"</div>";
|
||
});
|
||
</script>
|
||
</body>
|
||
|
||
</html>
|