583 lines
19 KiB
HTML
583 lines
19 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>Notes | 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="Notes" />
|
||
<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/19.08/Notes/" />
|
||
<meta property="og:url" content="https://plfa.github.io/19.08/Notes/" />
|
||
<meta property="og:site_name" content="Programming Language Foundations in Agda" />
|
||
<script type="application/ld+json">
|
||
{"url":"https://plfa.github.io/19.08/Notes/","headline":"Notes","description":"Programming Language Foundations in Agda","@type":"WebPage","@context":"https://schema.org"}</script>
|
||
<!-- End Jekyll SEO tag -->
|
||
<link rel="stylesheet" href="/19.08/assets/main.css"></head>
|
||
<body><header class="site-header" role="banner">
|
||
|
||
<div class="wrapper">
|
||
|
||
<a class="site-title" href="/19.08/">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="/19.08/">The Book</a>
|
||
<a class="page-link" href="/19.08/Announcements/">Announcements</a>
|
||
<a class="page-link" href="/19.08/GettingStarted/">Getting Started</a>
|
||
<a class="page-link" href="/19.08/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">Notes</h1>
|
||
</header>
|
||
|
||
<p style="text-align:center;">
|
||
|
||
|
||
|
||
|
||
|
||
</p>
|
||
|
||
|
||
<div class="post-content">
|
||
<h2 id="google-analytics">Google Analytics</h2>
|
||
|
||
<p><a href="https://analytics.google.com/analytics/web/">https://analytics.google.com/analytics/web/</a></p>
|
||
|
||
<h2 id="git-commands">Git commands</h2>
|
||
|
||
<p>Git commands to create a branch and pull request</p>
|
||
|
||
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>git help <command> -- get help on <command>
|
||
git branch -- list all branches
|
||
git branch <name> -- create new local branch <name>
|
||
git checkout <name> -- make <name> the current branch
|
||
git merge <name> -- merge branch <name> into current branch
|
||
git push origin <name> -- make local branch <name> into remote
|
||
</code></pre></div></div>
|
||
|
||
<p>On website, use pulldown menu to swith branch and then
|
||
click “new pull request” button.</p>
|
||
|
||
<h2 id="suggestion-from-conor-for-inference">Suggestion from Conor for Inference</h2>
|
||
|
||
<p>Conor McBride <a href="mailto:conor.mcbride@strath.ac.uk">conor.mcbride@strath.ac.uk</a></p>
|
||
|
||
<p>29 Oct 2018, 09:34</p>
|
||
|
||
<p>Hi Phil</p>
|
||
|
||
<p>In a rush, but…</p>
|
||
|
||
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>data Tag : Set where
|
||
tag-ℕ : Tag
|
||
tag-⇒ : Tag
|
||
</code></pre></div></div>
|
||
|
||
<p>…that’s just Bool. Bool is almost never your friend.</p>
|
||
|
||
<p>Get evidence!</p>
|
||
|
||
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>-- yer types
|
||
data Type : Set where
|
||
nat : Type
|
||
_=>_ : Type -> Type -> Type
|
||
|
||
-- logic
|
||
data Zero : Set where
|
||
record One : Set where constructor <>
|
||
|
||
-- evidence of not being =>
|
||
Not=> : Type -> Set
|
||
Not=> (_ => _) = Zero
|
||
Not=> _ = One
|
||
|
||
-- constructing the "=> or not" view
|
||
data Is=>? : Type -> Set where
|
||
is=> : (S T : Type) -> Is=>? (S => T)
|
||
not=> : {T : Type} -> Not=> T -> Is=>? T
|
||
|
||
-- this will need all n cases, but you do it once
|
||
is=>? : (T : Type) -> Is=>? T
|
||
is=>? nat = not=> <>
|
||
is=>? (S => T) = is=> _ _
|
||
|
||
-- worked example: domain
|
||
data Maybe (X : Set) : Set where
|
||
yes : X -> Maybe X
|
||
no : Maybe X
|
||
|
||
-- only two cases
|
||
dom : Type -> Maybe Type
|
||
dom T with is=>? T
|
||
dom .(S => T) | is=> S T = yes S
|
||
dom T | not=> p = no
|
||
|
||
-- addendum: in the not=> p case, if we subsequently inspect T, we can rule out the => case using p
|
||
{- with T
|
||
dom T | not=> p | nat = no
|
||
dom T | not=> () | q => q₁
|
||
-}
|
||
</code></pre></div></div>
|
||
|
||
<blockquote>
|
||
<p>We want to alert you that you’ve been granted the following access:
|
||
Manage Users and Edit
|
||
to the Google Analytics account <code class="language-plaintext highlighter-rouge">plfa (UA-125055580)</code> by <code class="language-plaintext highlighter-rouge">wen.kokke@gmail.com</code>.</p>
|
||
</blockquote>
|
||
|
||
<blockquote>
|
||
<p><a href="https://analytics.google.com/analytics/web/">Google analytics</a></p>
|
||
</blockquote>
|
||
|
||
<h2 id="where-to-put-lists">Where to put Lists?</h2>
|
||
|
||
<p>Three possible orders:</p>
|
||
<ul>
|
||
<li>(a) As current</li>
|
||
<li>(b) Put Lists immediately after Induction.
|
||
<ul>
|
||
<li>requires moving composition & extensionality earlier</li>
|
||
<li>requires moving parameterised modules earlier for monoids</li>
|
||
<li>add material to relations:
|
||
lexical ordering, subtype ordering, All, Any, All-++ iff</li>
|
||
<li>add material to isomorphism: All-++ isomorphism</li>
|
||
<li>retain material on decidability of All, Any in Decidable</li>
|
||
</ul>
|
||
</li>
|
||
<li>(c) Put Lists after Decidable
|
||
<ul>
|
||
<li>requires moving Any-decidable from Decidable to Lists</li>
|
||
</ul>
|
||
</li>
|
||
<li>(d) As (b) but put parameterised modules in a separate chapter</li>
|
||
</ul>
|
||
|
||
<p>Tradeoffs:</p>
|
||
<ul>
|
||
<li>(b) Distribution of exercises near where material is taught</li>
|
||
<li>(b) Additional reinforcement for simple proofs by induction</li>
|
||
<li>(a,c) Can drop material if there is lack of time</li>
|
||
<li>(a,c) Earlier emphasis on induction over evidence</li>
|
||
<li>(c) More consistent structuring principle</li>
|
||
</ul>
|
||
|
||
<h2 id="set-up-lists-of-exercises-to-do">Set up lists of exercises to do</h2>
|
||
|
||
<ul>
|
||
<li>Use md rather than HTML</li>
|
||
<li>Tell students to do <em>all</em> exercises, and just mark some as stretch?</li>
|
||
<li>Make a list of exercises to do, with some marked as stretch?</li>
|
||
<li>Compare with previous set of exercises to discover some holes?</li>
|
||
<li>Add ==N as an exercise to Relations?</li>
|
||
</ul>
|
||
|
||
<h2 id="other-questions">Other questions</h2>
|
||
|
||
<ul>
|
||
<li>Resolve any issues with modules to define properties of orderings?</li>
|
||
<li>Resolve any issues with equivalence and Setoids?</li>
|
||
</ul>
|
||
|
||
<h1 id="old-questions">Old questions</h1>
|
||
|
||
<h2 id="possible-structures-for-the-book">Possible structures for the book</h2>
|
||
|
||
<ul>
|
||
<li>One possible development
|
||
<ul>
|
||
<li>raw terms</li>
|
||
<li>scoped terms (is conversion from raw to scoped a function?)</li>
|
||
<li>typed terms (via bidirectional typing)</li>
|
||
</ul>
|
||
</li>
|
||
<li>The above could be developed either for
|
||
<ul>
|
||
<li>pure lambda terms with full normalisation</li>
|
||
<li>PCF with top-level reduction to value</li>
|
||
</ul>
|
||
</li>
|
||
<li>If I follow raw-scoped-typed then:
|
||
<ul>
|
||
<li>might want to have reductions for completely raw terms
|
||
later in the book rather than earlier</li>
|
||
<li>full normalisation requires substitution of open terms</li>
|
||
</ul>
|
||
</li>
|
||
<li>Today’s task (Tue 8 May)
|
||
<ul>
|
||
<li>consider lambda terms to values (not PCF)</li>
|
||
<li>
|
||
<p>raw, scoped, typed</p>
|
||
</li>
|
||
<li>Note that substitution for open terms is not hard,
|
||
it is proving it correct that is difficult!</li>
|
||
<li>can put each development in a separate module
|
||
to support reuse of names</li>
|
||
</ul>
|
||
</li>
|
||
<li>Today’s thoughts (Thu 10 May)
|
||
<ul>
|
||
<li>simplify TypedFresh
|
||
<ul>
|
||
<li>Does it become easier once I have
|
||
suitable lemmas about free in place?</li>
|
||
</ul>
|
||
</li>
|
||
<li>still need a chain of development
|
||
<ul>
|
||
<li>raw -> scoped -> typed</li>
|
||
<li>raw -> typed and typed -> raw needed for examples</li>
|
||
<li>look again at raw to scoped</li>
|
||
<li>look at scoped to typed</li>
|
||
<li>typed to raw requires fresh names</li>
|
||
<li>fresh name strategy: primed or numbers?</li>
|
||
<li>ops on strings: show, read, strip from end</li>
|
||
</ul>
|
||
</li>
|
||
<li>trickier ideas
|
||
<ul>
|
||
<li>factor TypedFresh into Barendregt followed
|
||
by substitution? This might actually lead
|
||
to a much longer development</li>
|
||
<li>would be cool if Barendregt never required
|
||
renaming in case of substitution by closed
|
||
terms, but I think this is hard</li>
|
||
</ul>
|
||
</li>
|
||
</ul>
|
||
</li>
|
||
<li>Today’s achievements and next steps (Thu 10 May)
|
||
<ul>
|
||
<li>defined break, make to extract a prefix
|
||
and count primes at end of an id. But hard
|
||
to do corresponding proofs. Need to figure out
|
||
how to exploit abstraction to make terms readable.</li>
|
||
<li>Conversion of raw to scoped and scoped to raw
|
||
is easy if I use impossible</li>
|
||
<li>Added conversion of TypedDB to PHOAS in
|
||
extra/DeBruijn-agda-list-4.lagda</li>
|
||
<li>Next: try adding bidirectional typing to
|
||
convert Raw or Scoped to TypedDB</li>
|
||
<li>Next: Can proofs in Typed be simplified by
|
||
applying suitable lemmas about free?</li>
|
||
<li>updated Agda from:
|
||
Agda version 2.6.0-4654bfb-dirty
|
||
to:
|
||
Agda version 2.6.0-2f2f4f5
|
||
Now TypedFresh.lagda computes 2+2 in milliseconds
|
||
(as opposed to failing to compute it in one day).</li>
|
||
</ul>
|
||
</li>
|
||
</ul>
|
||
|
||
<h2 id="stlc">STLC</h2>
|
||
|
||
<ul>
|
||
<li>Russel O’Connor
|
||
<ul>
|
||
<li>STLC with recursive types, intrinsic representation
|
||
<ul>
|
||
<li>https://hub.darcs.net/roconnor/STLC/browse/src/STLC</li>
|
||
</ul>
|
||
</li>
|
||
</ul>
|
||
</li>
|
||
</ul>
|
||
|
||
<h2 id="phoas">PHOAS</h2>
|
||
|
||
<p>The following comments were collected on the Agda mailing list.</p>
|
||
|
||
<ul>
|
||
<li>Nils Anders Danielsson <a href="mailto:nad@cse.gu.se">nad@cse.gu.se</a>
|
||
<ul>
|
||
<li>cites Chlipala, who uses binary parametricity
|
||
<ul>
|
||
<li>http://adam.chlipala.net/cpdt/html/Cpdt.ProgLang.html</li>
|
||
<li>http://adam.chlipala.net/cpdt/html/Intensional.html</li>
|
||
</ul>
|
||
</li>
|
||
</ul>
|
||
</li>
|
||
<li>Roman <a href="mailto:effectfully@gmail.com">effectfully@gmail.com</a>
|
||
<ul>
|
||
<li>(similar to my solution)
|
||
<ul>
|
||
<li>https://github.com/effectfully/random-stuff/blob/master/Normalization/PHOAS.agda</li>
|
||
<li>https://github.com/effectfully/random-stuff/blob/master/Normalization/Liftable.agda</li>
|
||
</ul>
|
||
</li>
|
||
<li>also cites Abel’s habilitation
|
||
<ul>
|
||
<li>http://www.cse.chalmers.se/~abela/habil.pdf</li>
|
||
</ul>
|
||
</li>
|
||
<li>See his note to the Agda mailing list of 26 June,
|
||
“Typed Jigger in vanilla Agda”
|
||
It points to the following solution.
|
||
<ul>
|
||
<li>https://github.com/effectfully/random-stuff/blob/master/TypedJigger.agda</li>
|
||
</ul>
|
||
</li>
|
||
</ul>
|
||
</li>
|
||
<li>András Kovács <a href="mailto:kovacsahun@hotmail.com">kovacsahun@hotmail.com</a>
|
||
<ul>
|
||
<li>applies unary parametricity
|
||
<ul>
|
||
<li>http://lpaste.net/363029</li>
|
||
</ul>
|
||
</li>
|
||
</ul>
|
||
</li>
|
||
<li>Ulf Norell <a href="mailto:ulf.norell@gmail.com">ulf.norell@gmail.com</a>
|
||
<ul>
|
||
<li>helped with deriving Eq</li>
|
||
</ul>
|
||
</li>
|
||
<li>David Darais (not on mailing list)
|
||
<ul>
|
||
<li>suggests Scoped PHOAS
|
||
<ul>
|
||
<li>https://plum-umd.github.io/darailude-agda/SF.PHOAS.html</li>
|
||
</ul>
|
||
</li>
|
||
</ul>
|
||
</li>
|
||
</ul>
|
||
|
||
<h2 id="untyped-lambda-calculus">Untyped lambda calculus</h2>
|
||
|
||
<ul>
|
||
<li>Nils Anders Danielsson <a href="mailto:nad@cse.gu.se">nad@cse.gu.se</a>
|
||
+
|
||
http://www.cse.chalmers.se/~nad/listings/partiality-monad/Lambda.Simplified.Delay-monad.Interpreter.html
|
||
<ul>
|
||
<li>/~nad/repos/codata/Lambda/Closure/Functional</li>
|
||
</ul>
|
||
</li>
|
||
<li>untyped lambda calculus by Gallais
|
||
<ul>
|
||
<li>https://gist.github.com/gallais/303cfcfe053fbc63eb61</li>
|
||
</ul>
|
||
</li>
|
||
<li>lambda calculus
|
||
<ul>
|
||
<li>https://github.com/pi8027/lambda-calculus/tree/master/agda/Lambda</li>
|
||
</ul>
|
||
</li>
|
||
</ul>
|
||
|
||
<h2 id="relevant-papers">Relevant papers</h2>
|
||
|
||
<ul>
|
||
<li>Kenichi Asai, Extracting a Call-by-Name Partial Evaluator from a Proof of
|
||
Termination, PEPM 2019
|
||
<ul>
|
||
<li>http://pllab.is.ocha.ac.jp/~asai/papers/pepm19.pdf</li>
|
||
<li>http://pllab.is.ocha.ac.jp/~asai/papers/pepm2019/</li>
|
||
</ul>
|
||
</li>
|
||
<li>Kenichi Asai, Certifying CPS Transformation of Let-Polymorphic
|
||
Calculus Using PHOAS, APLAS 2018
|
||
<ul>
|
||
<li>https://link.springer.com/chapter/10.1007/978-3-030-02768-1_20</li>
|
||
<li>http://pllab.is.ocha.ac.jp/~asai/papers/aplas18.agda</li>
|
||
</ul>
|
||
</li>
|
||
</ul>
|
||
|
||
<h2 id="agda-resources">Agda resources</h2>
|
||
<ul>
|
||
<li>Chalmers class
|
||
<ul>
|
||
<li>http://www.cse.chalmers.se/edu/year/2017/course/DAT140_Types/</li>
|
||
</ul>
|
||
</li>
|
||
<li>Dybjer lecture notes
|
||
<ul>
|
||
<li>http://www.cse.chalmers.se/edu/year/2017/course/DAT140_Types/LectureNotes.pdf</li>
|
||
</ul>
|
||
</li>
|
||
<li>Ulf Norell and James Chapman lecture notes
|
||
<ul>
|
||
<li>http://www.cse.chalmers.se/~ulfn/darcs/AFP08/LectureNotes/AgdaIntro.pdf</li>
|
||
</ul>
|
||
</li>
|
||
<li>Chalmer Take Home exam 2017
|
||
<ul>
|
||
<li>http://www.cse.chalmers.se/edu/year/2017/course/DAT140_Types/TakeHomeExamTypes2017.pdf</li>
|
||
</ul>
|
||
</li>
|
||
</ul>
|
||
|
||
<h2 id="syntax-for-lambda-calculus">Syntax for lambda calculus</h2>
|
||
|
||
<ul>
|
||
<li>ƛ \Gl-</li>
|
||
<li>∙ .</li>
|
||
</ul>
|
||
|
||
|
||
</div>
|
||
|
||
<p style="text-align:center;">
|
||
|
||
|
||
|
||
|
||
|
||
</p>
|
||
|
||
|
||
</article>
|
||
|
||
</div>
|
||
</main><footer class="site-footer h-card">
|
||
<data class="u-url" href="/19.08/"></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="/19.08/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="/19.08/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="/19.08/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 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="/19.08/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="/19.08/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="/19.08/assets/jquery.js"></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="/19.08/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>
|