677 lines
24 KiB
HTML
677 lines
24 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/20.07/Notes/" />
|
||
<meta property="og:url" content="https://plfa.github.io/20.07/Notes/" />
|
||
<meta property="og:site_name" content="Programming Language Foundations in Agda" />
|
||
<script type="application/ld+json">
|
||
{"url":"https://plfa.github.io/20.07/Notes/","headline":"Notes","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">Notes</h1>
|
||
</header>
|
||
|
||
<p style="text-align:center;">
|
||
|
||
|
||
|
||
|
||
|
||
</p>
|
||
|
||
|
||
<div class="post-content">
|
||
<h2 id="to-do">To Do</h2>
|
||
|
||
<p>Changes I would like to make to the book:</p>
|
||
<ul>
|
||
<li>Relations, exercise <code class="language-plaintext highlighter-rouge">o+o≡e</code> –> (recommended)</li>
|
||
<li>Relations, exercise <code class="language-plaintext highlighter-rouge">≤-iff-<</code> –> <code class="language-plaintext highlighter-rouge">≤→<</code>, <code class="language-plaintext highlighter-rouge"><→≤</code></li>
|
||
<li>Relations, exercise <code class="language-plaintext highlighter-rouge">Bin-predicates</code> –> <code class="language-plaintext highlighter-rouge">Bin-predicate</code>
|
||
change canonical form of zero to be empty string, <code class="language-plaintext highlighter-rouge"><></code>.
|
||
Similar change to subsequent exercise.</li>
|
||
</ul>
|
||
|
||
<h2 id="downloading-older-versions">Downloading older versions</h2>
|
||
|
||
<p><a href="https://github.com/plfa/plfa.github.io/releases">https://github.com/plfa/plfa.github.io/releases</a></p>
|
||
|
||
<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>
|
||
|
||
<h2 id="adrians-comments-from-meetup">Adrian’s comments from MeetUp</h2>
|
||
|
||
<p>Adrian King
|
||
I think we’ve finally gone through the whole book now up through chapter Properties, and we’ve come up with just three places where we thought the book could have done a better job of preparing us for the exercises.</p>
|
||
|
||
<p>Starting from the end of the book:</p>
|
||
|
||
<ul>
|
||
<li>Chapter Quantifiers, exercise Bin-isomorphism:</li>
|
||
</ul>
|
||
|
||
<p>In the to∘from case, we want to show that:</p>
|
||
|
||
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>⟨ to (from x) , toCan {from x} ⟩ ≡ ⟨ x , canX ⟩
|
||
</code></pre></div></div>
|
||
|
||
<p>I found myself wanting to use a general lemma like:</p>
|
||
|
||
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>exEq :
|
||
∀ {A : Set} {x y : A} {p : A → Set} {px : p x} {py : p y} →
|
||
x ≡ y →
|
||
px ≡ py →
|
||
⟨ x , px ⟩ ≡ ⟨ y , py ⟩
|
||
exEq refl refl = refl
|
||
</code></pre></div></div>
|
||
|
||
<p>which is in some sense true, but in Agda it doesn’t typecheck, because Agda can’t see that px’s type and py’s type are the same. My solution made explicit use of heterogeneous equality.</p>
|
||
|
||
<p>I realize there are ways to solve this that don’t explicitly use heterogeneous equality, but the surprise factor of the exercise might have been lower if heterogeneous equality had been mentioned by that point, perhaps in the Equality chapter.</p>
|
||
|
||
<ul>
|
||
<li>Chapter Quantifiers, exercise ∀-×:</li>
|
||
</ul>
|
||
|
||
<p>I assume the intended solution looks something like:</p>
|
||
|
||
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>∀-× : ∀ {B : Tri → Set} → ((x : Tri) → B x) ≃ (B aa × B bb × B cc)
|
||
∀-× = record {
|
||
to = λ f → ⟨ f aa , ⟨ f bb , f cc ⟩ ⟩ ;
|
||
from = λ{ ⟨ baa , ⟨ bbb , bcc ⟩ ⟩ → λ{ aa → baa ; bb → bbb ; cc → bcc } } ;
|
||
from∘to = λ f → extensionality λ{ aa → refl ; bb → refl ; cc → refl } ;
|
||
to∘from = λ{ y → refl } }
|
||
</code></pre></div></div>
|
||
|
||
<p>but it doesn’t typecheck; in the extensionality presented earlier (in chapter Isomorphism), type B is not dependent on type A, but it needs to be here. Agda’s error message is sufficiently baffling here that you might want to warn people that they need a dependent version of extensionality, something like:</p>
|
||
|
||
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>Extensionality : (a b : Level) → Set _
|
||
Extensionality a b =
|
||
{A : Set a} {B : A → Set b} {f g : (x : A) → B x} →
|
||
(∀ x → f x ≡ g x) → f ≡ g
|
||
|
||
postulate
|
||
exten : ∀ {a b} → Extensionality a b
|
||
</code></pre></div></div>
|
||
|
||
<ul>
|
||
<li>Chapter Relations, exercise Bin-predicates:</li>
|
||
</ul>
|
||
|
||
<p>I made use here of the inspect idiom, in Aaron Stump’s variant, which is syntactically more convenient:</p>
|
||
|
||
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>keep : ∀ {ℓa} → {a : Set ℓa} → (x : a) → Σ a (λ y → y ≡ x)
|
||
keep x = x , refl
|
||
</code></pre></div></div>
|
||
|
||
<p>Pattern matching on keep m, where m is some complicated term, lets you keep around an equality between the original term and the pattern matched, which is often convenient, as in:</p>
|
||
|
||
<div class="language-plaintext highlighter-rouge"><div class="highlight"><pre class="highlight"><code>roundTripTwice {x} onex with keep (from x)
|
||
roundTripTwice {x} onex | zero , eq with oneIsMoreThanZero onex
|
||
roundTripTwice {x} onex | zero , eq | 0<fromx rewrite sym eq =
|
||
⊥-elim (not0<0 0<fromx)
|
||
roundTripTwice {x} onex | suc n , eq rewrite sym eq | toTwiceSuc {n} |
|
||
cong x0_ (sym (roundTrip (one onex))) | sym eq = refl
|
||
</code></pre></div></div>
|
||
|
||
</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>
|